H-Termination proof of /home/matraf/haskell/eval_FullyBlown

YES 3.464 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:

↳ HASKELL

  ↳ CR

mainModule List

((sort :: [Int] -> [Int]) :: [Int] -> [Int])

module List where

import qualified Maybe
import qualified Prelude

merge :: (a -> a -> Ordering) -> [a] -> [a] -> [a]

merge

cmp xs []

merge

cmp [] ys

merge

cmp (x : xs) (y : ys)

case	x `cmp` y of
	GT	->	y : merge cmp (x : xs) ys
	_	->	x : merge cmp xs (y : ys)

merge_pairs :: (a -> a -> Ordering) -> [[a]] -> [[a]]

merge_pairs	cmp []	=	[]
merge_pairs	cmp (xs : [])	=	xs : []
merge_pairs	cmp (xs : ys : xss)	=	merge cmp xs ys : merge_pairs cmp xss

mergesort :: (a -> a -> Ordering) -> [a] -> [a]

mergesort

cmp

mergesort' cmp . map wrap

mergesort' :: (a -> a -> Ordering) -> [[a]] -> [a]

mergesort'	cmp []	=	[]
mergesort'	cmp (xs : [])	=	xs
mergesort'	cmp xss	=	mergesort' cmp (merge_pairs cmp xss)

sort :: Ord a => [a] -> [a]

sort

mergesort compare l

wrap :: a -> [a]

wrap

x : []

module Maybe where

import qualified List
import qualified Prelude

Case Reductions:
The following Case expression

case cmp x y of
GT → y : merge cmp (x : xs) ys

_ → x : merge cmp xs (y : ys)

is transformed to

merge0 y cmp x xs ys GT = y : merge cmp (x : xs) ys

merge0 y cmp x xs ys _ = x : merge cmp xs (y : ys)

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

mainModule List

((sort :: [Int] -> [Int]) :: [Int] -> [Int])

module List where

import qualified Maybe
import qualified Prelude

merge :: (a -> a -> Ordering) -> [a] -> [a] -> [a]

merge	cmp xs []	=	xs
merge	cmp [] ys	=	ys
merge	cmp (x : xs) (y : ys)	=	merge0 y cmp x xs ys (x `cmp` y)

merge0	y cmp x xs ys GT	=	y : merge cmp (x : xs) ys
merge0	y cmp x xs ys _	=	x : merge cmp xs (y : ys)

merge_pairs :: (a -> a -> Ordering) -> [[a]] -> [[a]]

merge_pairs	cmp []	=	[]
merge_pairs	cmp (xs : [])	=	xs : []
merge_pairs	cmp (xs : ys : xss)	=	merge cmp xs ys : merge_pairs cmp xss

mergesort :: (a -> a -> Ordering) -> [a] -> [a]

mergesort

cmp

mergesort' cmp . map wrap

mergesort' :: (a -> a -> Ordering) -> [[a]] -> [a]

mergesort'	cmp []	=	[]
mergesort'	cmp (xs : [])	=	xs
mergesort'	cmp xss	=	mergesort' cmp (merge_pairs cmp xss)

sort :: Ord a => [a] -> [a]

sort

mergesort compare l

wrap :: a -> [a]

wrap

x : []

module Maybe where

import qualified List
import qualified Prelude

Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

mainModule List

((sort :: [Int] -> [Int]) :: [Int] -> [Int])

module List where

import qualified Maybe
import qualified Prelude

merge :: (a -> a -> Ordering) -> [a] -> [a] -> [a]

merge	cmp xs []	=	xs
merge	cmp [] ys	=	ys
merge	cmp (x : xs) (y : ys)	=	merge0 y cmp x xs ys (x `cmp` y)

merge0	y cmp x xs ys GT	=	y : merge cmp (x : xs) ys
merge0	y cmp x xs ys vw	=	x : merge cmp xs (y : ys)

merge_pairs :: (a -> a -> Ordering) -> [[a]] -> [[a]]

merge_pairs	cmp []	=	[]
merge_pairs	cmp (xs : [])	=	xs : []
merge_pairs	cmp (xs : ys : xss)	=	merge cmp xs ys : merge_pairs cmp xss

mergesort :: (a -> a -> Ordering) -> [a] -> [a]

mergesort

cmp

mergesort' cmp . map wrap

mergesort' :: (a -> a -> Ordering) -> [[a]] -> [a]

mergesort'	cmp []	=	[]
mergesort'	cmp (xs : [])	=	xs
mergesort'	cmp xss	=	mergesort' cmp (merge_pairs cmp xss)

sort :: Ord a => [a] -> [a]

sort

mergesort compare l

wrap :: a -> [a]

wrap

x : []

module Maybe where

import qualified List
import qualified Prelude

Cond Reductions:
The following Function with conditions

undefined

| False

= undefined

is transformed to

undefined = undefined1

undefined0 True = undefined

undefined1 = undefined0 False

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

mainModule List

(sort :: [Int] -> [Int])

module List where

import qualified Maybe
import qualified Prelude

merge :: (a -> a -> Ordering) -> [a] -> [a] -> [a]

merge	cmp xs []	=	xs
merge	cmp [] ys	=	ys
merge	cmp (x : xs) (y : ys)	=	merge0 y cmp x xs ys (x `cmp` y)

merge0	y cmp x xs ys GT	=	y : merge cmp (x : xs) ys
merge0	y cmp x xs ys vw	=	x : merge cmp xs (y : ys)

merge_pairs :: (a -> a -> Ordering) -> [[a]] -> [[a]]

merge_pairs	cmp []	=	[]
merge_pairs	cmp (xs : [])	=	xs : []
merge_pairs	cmp (xs : ys : xss)	=	merge cmp xs ys : merge_pairs cmp xss

mergesort :: (a -> a -> Ordering) -> [a] -> [a]

mergesort

cmp

mergesort' cmp . map wrap

mergesort' :: (a -> a -> Ordering) -> [[a]] -> [a]

mergesort'	cmp []	=	[]
mergesort'	cmp (xs : [])	=	xs
mergesort'	cmp xss	=	mergesort' cmp (merge_pairs cmp xss)

sort :: Ord a => [a] -> [a]

sort

mergesort compare l

wrap :: a -> [a]

wrap

x : []

module Maybe where

import qualified List
import qualified Prelude

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="sort",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="sort vz3",fontsize=16,color="black",shape="triangle"];3 -> 4[label="",style="solid", color="black", weight=3];
4[label="mergesort compare vz3",fontsize=16,color="black",shape="box"];4 -> 5[label="",style="solid", color="black", weight=3];
5[label="(mergesort' compare) . map wrap",fontsize=16,color="black",shape="box"];5 -> 6[label="",style="solid", color="black", weight=3];
6[label="mergesort' compare (map wrap vz3)",fontsize=16,color="burlywood",shape="box"];1464[label="vz3/vz30 : vz31",fontsize=10,color="white",style="solid",shape="box"];6 -> 1464[label="",style="solid", color="burlywood", weight=9];
1464 -> 7[label="",style="solid", color="burlywood", weight=3];
1465[label="vz3/[]",fontsize=10,color="white",style="solid",shape="box"];6 -> 1465[label="",style="solid", color="burlywood", weight=9];
1465 -> 8[label="",style="solid", color="burlywood", weight=3];
7[label="mergesort' compare (map wrap (vz30 : vz31))",fontsize=16,color="black",shape="box"];7 -> 9[label="",style="solid", color="black", weight=3];
8[label="mergesort' compare (map wrap [])",fontsize=16,color="black",shape="box"];8 -> 10[label="",style="solid", color="black", weight=3];
9[label="mergesort' compare (wrap vz30 : map wrap vz31)",fontsize=16,color="burlywood",shape="box"];1466[label="vz31/vz310 : vz311",fontsize=10,color="white",style="solid",shape="box"];9 -> 1466[label="",style="solid", color="burlywood", weight=9];
1466 -> 11[label="",style="solid", color="burlywood", weight=3];
1467[label="vz31/[]",fontsize=10,color="white",style="solid",shape="box"];9 -> 1467[label="",style="solid", color="burlywood", weight=9];
1467 -> 12[label="",style="solid", color="burlywood", weight=3];
10[label="mergesort' compare []",fontsize=16,color="black",shape="box"];10 -> 13[label="",style="solid", color="black", weight=3];
11[label="mergesort' compare (wrap vz30 : map wrap (vz310 : vz311))",fontsize=16,color="black",shape="box"];11 -> 14[label="",style="solid", color="black", weight=3];
12[label="mergesort' compare (wrap vz30 : map wrap [])",fontsize=16,color="black",shape="box"];12 -> 15[label="",style="solid", color="black", weight=3];
13[label="[]",fontsize=16,color="green",shape="box"];14[label="mergesort' compare (wrap vz30 : wrap vz310 : map wrap vz311)",fontsize=16,color="black",shape="box"];14 -> 16[label="",style="solid", color="black", weight=3];
15[label="mergesort' compare (wrap vz30 : [])",fontsize=16,color="black",shape="box"];15 -> 17[label="",style="solid", color="black", weight=3];
16[label="mergesort' compare (merge_pairs compare (wrap vz30 : wrap vz310 : map wrap vz311))",fontsize=16,color="black",shape="box"];16 -> 18[label="",style="solid", color="black", weight=3];
17[label="wrap vz30",fontsize=16,color="black",shape="triangle"];17 -> 19[label="",style="solid", color="black", weight=3];
18 -> 1042[label="",style="dashed", color="red", weight=0];
18[label="mergesort' compare (merge compare (wrap vz30) (wrap vz310) : merge_pairs compare (map wrap vz311))",fontsize=16,color="magenta"];18 -> 1043[label="",style="dashed", color="magenta", weight=3];
18 -> 1044[label="",style="dashed", color="magenta", weight=3];
19[label="vz30 : []",fontsize=16,color="green",shape="box"];1043 -> 1197[label="",style="dashed", color="red", weight=0];
1043[label="merge compare (wrap vz30) (wrap vz310)",fontsize=16,color="magenta"];1043 -> 1198[label="",style="dashed", color="magenta", weight=3];
1043 -> 1199[label="",style="dashed", color="magenta", weight=3];
1044[label="map wrap vz311",fontsize=16,color="burlywood",shape="triangle"];1470[label="vz311/vz3110 : vz3111",fontsize=10,color="white",style="solid",shape="box"];1044 -> 1470[label="",style="solid", color="burlywood", weight=9];
1470 -> 1200[label="",style="solid", color="burlywood", weight=3];
1471[label="vz311/[]",fontsize=10,color="white",style="solid",shape="box"];1044 -> 1471[label="",style="solid", color="burlywood", weight=9];
1471 -> 1201[label="",style="solid", color="burlywood", weight=3];
1042[label="mergesort' compare (vz117 : merge_pairs compare vz118)\n  Ord a",fontsize=16,color="burlywood",shape="triangle"];1472[label="vz118/vz1180 : vz1181",fontsize=10,color="white",style="solid",shape="box"];1042 -> 1472[label="",style="solid", color="burlywood", weight=9];
1472 -> 1202[label="",style="solid", color="burlywood", weight=3];
1473[label="vz118/[]",fontsize=10,color="white",style="solid",shape="box"];1042 -> 1473[label="",style="solid", color="burlywood", weight=9];
1473 -> 1203[label="",style="solid", color="burlywood", weight=3];
1198 -> 17[label="",style="dashed", color="red", weight=0];
1198[label="wrap vz310",fontsize=16,color="magenta"];1198 -> 1204[label="",style="dashed", color="magenta", weight=3];
1199 -> 17[label="",style="dashed", color="red", weight=0];
1199[label="wrap vz30",fontsize=16,color="magenta"];1197[label="merge compare vz120 vz119",fontsize=16,color="burlywood",shape="triangle"];1476[label="vz119/vz1190 : vz1191",fontsize=10,color="white",style="solid",shape="box"];1197 -> 1476[label="",style="solid", color="burlywood", weight=9];
1476 -> 1205[label="",style="solid", color="burlywood", weight=3];
1477[label="vz119/[]",fontsize=10,color="white",style="solid",shape="box"];1197 -> 1477[label="",style="solid", color="burlywood", weight=9];
1477 -> 1206[label="",style="solid", color="burlywood", weight=3];
1200[label="map wrap (vz3110 : vz3111)",fontsize=16,color="black",shape="box"];1200 -> 1207[label="",style="solid", color="black", weight=3];
1201[label="map wrap []",fontsize=16,color="black",shape="box"];1201 -> 1208[label="",style="solid", color="black", weight=3];
1202[label="mergesort' compare (vz117 : merge_pairs compare (vz1180 : vz1181))\n  Ord a",fontsize=16,color="burlywood",shape="box"];1478[label="vz1181/vz11810 : vz11811",fontsize=10,color="white",style="solid",shape="box"];1202 -> 1478[label="",style="solid", color="burlywood", weight=9];
1478 -> 1209[label="",style="solid", color="burlywood", weight=3];
1479[label="vz1181/[]",fontsize=10,color="white",style="solid",shape="box"];1202 -> 1479[label="",style="solid", color="burlywood", weight=9];
1479 -> 1210[label="",style="solid", color="burlywood", weight=3];
1203[label="mergesort' compare (vz117 : merge_pairs compare [])\n  Ord a",fontsize=16,color="black",shape="box"];1203 -> 1211[label="",style="solid", color="black", weight=3];
1204[label="vz310",fontsize=16,color="green",shape="box"];1205[label="merge compare vz120 (vz1190 : vz1191)",fontsize=16,color="burlywood",shape="box"];1480[label="vz120/vz1200 : vz1201",fontsize=10,color="white",style="solid",shape="box"];1205 -> 1480[label="",style="solid", color="burlywood", weight=9];
1480 -> 1212[label="",style="solid", color="burlywood", weight=3];
1481[label="vz120/[]",fontsize=10,color="white",style="solid",shape="box"];1205 -> 1481[label="",style="solid", color="burlywood", weight=9];
1481 -> 1213[label="",style="solid", color="burlywood", weight=3];
1206[label="merge compare vz120 []",fontsize=16,color="black",shape="box"];1206 -> 1214[label="",style="solid", color="black", weight=3];
1207[label="wrap vz3110 : map wrap vz3111",fontsize=16,color="green",shape="box"];1207 -> 1215[label="",style="dashed", color="green", weight=3];
1207 -> 1216[label="",style="dashed", color="green", weight=3];
1208[label="[]",fontsize=16,color="green",shape="box"];1209[label="mergesort' compare (vz117 : merge_pairs compare (vz1180 : vz11810 : vz11811))\n  Ord a",fontsize=16,color="black",shape="box"];1209 -> 1217[label="",style="solid", color="black", weight=3];
1210[label="mergesort' compare (vz117 : merge_pairs compare (vz1180 : []))\n  Ord a",fontsize=16,color="black",shape="box"];1210 -> 1218[label="",style="solid", color="black", weight=3];
1211[label="mergesort' compare (vz117 : [])\n  Ord a",fontsize=16,color="black",shape="box"];1211 -> 1219[label="",style="solid", color="black", weight=3];
1212[label="merge compare (vz1200 : vz1201) (vz1190 : vz1191)",fontsize=16,color="black",shape="box"];1212 -> 1220[label="",style="solid", color="black", weight=3];
1213[label="merge compare [] (vz1190 : vz1191)",fontsize=16,color="black",shape="box"];1213 -> 1221[label="",style="solid", color="black", weight=3];
1214[label="vz120",fontsize=16,color="green",shape="box"];1215 -> 17[label="",style="dashed", color="red", weight=0];
1215[label="wrap vz3110",fontsize=16,color="magenta"];1215 -> 1222[label="",style="dashed", color="magenta", weight=3];
1216 -> 1044[label="",style="dashed", color="red", weight=0];
1216[label="map wrap vz3111",fontsize=16,color="magenta"];1216 -> 1223[label="",style="dashed", color="magenta", weight=3];
1217[label="mergesort' compare (vz117 : merge compare vz1180 vz11810 : merge_pairs compare vz11811)\n  Ord a",fontsize=16,color="black",shape="box"];1217 -> 1224[label="",style="solid", color="black", weight=3];
1218[label="mergesort' compare (vz117 : vz1180 : [])\n  Ord a",fontsize=16,color="black",shape="box"];1218 -> 1225[label="",style="solid", color="black", weight=3];
1219[label="vz117\n  Ord a",fontsize=16,color="green",shape="box"];1220 -> 1298[label="",style="dashed", color="red", weight=0];
1220[label="merge0 vz1190 compare vz1200 vz1201 vz1191 (compare vz1200 vz1190)",fontsize=16,color="magenta"];1220 -> 1299[label="",style="dashed", color="magenta", weight=3];
1220 -> 1300[label="",style="dashed", color="magenta", weight=3];
1220 -> 1301[label="",style="dashed", color="magenta", weight=3];
1220 -> 1302[label="",style="dashed", color="magenta", weight=3];
1220 -> 1303[label="",style="dashed", color="magenta", weight=3];
1221[label="vz1190 : vz1191",fontsize=16,color="green",shape="box"];1222[label="vz3110",fontsize=16,color="green",shape="box"];1223[label="vz3111",fontsize=16,color="green",shape="box"];1224[label="mergesort' compare (merge_pairs compare (vz117 : merge compare vz1180 vz11810 : merge_pairs compare vz11811))\n  Ord a",fontsize=16,color="black",shape="box"];1224 -> 1227[label="",style="solid", color="black", weight=3];
1225[label="mergesort' compare (merge_pairs compare (vz117 : vz1180 : []))\n  Ord a",fontsize=16,color="black",shape="box"];1225 -> 1228[label="",style="solid", color="black", weight=3];
1299[label="vz1191",fontsize=16,color="green",shape="box"];1300[label="vz1201",fontsize=16,color="green",shape="box"];1301[label="vz1200",fontsize=16,color="green",shape="box"];1302[label="vz1190",fontsize=16,color="green",shape="box"];1303[label="compare vz1200 vz1190",fontsize=16,color="black",shape="triangle"];1303 -> 1314[label="",style="solid", color="black", weight=3];
1298[label="merge0 vz127 compare vz128 vz129 vz130 vz131\n  Ord a",fontsize=16,color="burlywood",shape="triangle"];1485[label="vz131/LT",fontsize=10,color="white",style="solid",shape="box"];1298 -> 1485[label="",style="solid", color="burlywood", weight=9];
1485 -> 1315[label="",style="solid", color="burlywood", weight=3];
1486[label="vz131/EQ",fontsize=10,color="white",style="solid",shape="box"];1298 -> 1486[label="",style="solid", color="burlywood", weight=9];
1486 -> 1316[label="",style="solid", color="burlywood", weight=3];
1487[label="vz131/GT",fontsize=10,color="white",style="solid",shape="box"];1298 -> 1487[label="",style="solid", color="burlywood", weight=9];
1487 -> 1317[label="",style="solid", color="burlywood", weight=3];
1227 -> 1042[label="",style="dashed", color="red", weight=0];
1227[label="mergesort' compare (merge compare vz117 (merge compare vz1180 vz11810) : merge_pairs compare (merge_pairs compare vz11811))\n  Ord a",fontsize=16,color="magenta"];1227 -> 1231[label="",style="dashed", color="magenta", weight=3];
1227 -> 1232[label="",style="dashed", color="magenta", weight=3];
1228 -> 1042[label="",style="dashed", color="red", weight=0];
1228[label="mergesort' compare (merge compare vz117 vz1180 : merge_pairs compare [])\n  Ord a",fontsize=16,color="magenta"];1228 -> 1233[label="",style="dashed", color="magenta", weight=3];
1228 -> 1234[label="",style="dashed", color="magenta", weight=3];
1314[label="primCmpInt vz1200 vz1190",fontsize=16,color="burlywood",shape="box"];1490[label="vz1200/Pos vz12000",fontsize=10,color="white",style="solid",shape="box"];1314 -> 1490[label="",style="solid", color="burlywood", weight=9];
1490 -> 1349[label="",style="solid", color="burlywood", weight=3];
1491[label="vz1200/Neg vz12000",fontsize=10,color="white",style="solid",shape="box"];1314 -> 1491[label="",style="solid", color="burlywood", weight=9];
1491 -> 1350[label="",style="solid", color="burlywood", weight=3];
1315[label="merge0 vz127 compare vz128 vz129 vz130 LT\n  Ord a",fontsize=16,color="black",shape="box"];1315 -> 1351[label="",style="solid", color="black", weight=3];
1316[label="merge0 vz127 compare vz128 vz129 vz130 EQ\n  Ord a",fontsize=16,color="black",shape="box"];1316 -> 1352[label="",style="solid", color="black", weight=3];
1317[label="merge0 vz127 compare vz128 vz129 vz130 GT\n  Ord a",fontsize=16,color="black",shape="box"];1317 -> 1353[label="",style="solid", color="black", weight=3];
1231[label="merge compare vz117 (merge compare vz1180 vz11810)\n  Ord a",fontsize=16,color="burlywood",shape="box"];1492[label="vz11810/vz118100 : vz118101",fontsize=10,color="white",style="solid",shape="box"];1231 -> 1492[label="",style="solid", color="burlywood", weight=9];
1492 -> 1239[label="",style="solid", color="burlywood", weight=3];
1493[label="vz11810/[]",fontsize=10,color="white",style="solid",shape="box"];1231 -> 1493[label="",style="solid", color="burlywood", weight=9];
1493 -> 1240[label="",style="solid", color="burlywood", weight=3];
1232[label="merge_pairs compare vz11811\n  Ord a",fontsize=16,color="burlywood",shape="triangle"];1494[label="vz11811/vz118110 : vz118111",fontsize=10,color="white",style="solid",shape="box"];1232 -> 1494[label="",style="solid", color="burlywood", weight=9];
1494 -> 1241[label="",style="solid", color="burlywood", weight=3];
1495[label="vz11811/[]",fontsize=10,color="white",style="solid",shape="box"];1232 -> 1495[label="",style="solid", color="burlywood", weight=9];
1495 -> 1242[label="",style="solid", color="burlywood", weight=3];
1233[label="merge compare vz117 vz1180\n  Ord a",fontsize=16,color="burlywood",shape="triangle"];1496[label="vz1180/vz11800 : vz11801",fontsize=10,color="white",style="solid",shape="box"];1233 -> 1496[label="",style="solid", color="burlywood", weight=9];
1496 -> 1243[label="",style="solid", color="burlywood", weight=3];
1497[label="vz1180/[]",fontsize=10,color="white",style="solid",shape="box"];1233 -> 1497[label="",style="solid", color="burlywood", weight=9];
1497 -> 1244[label="",style="solid", color="burlywood", weight=3];
1234[label="[]\n  Ord a",fontsize=16,color="green",shape="box"];1349[label="primCmpInt (Pos vz12000) vz1190",fontsize=16,color="burlywood",shape="box"];1498[label="vz12000/Succ vz120000",fontsize=10,color="white",style="solid",shape="box"];1349 -> 1498[label="",style="solid", color="burlywood", weight=9];
1498 -> 1397[label="",style="solid", color="burlywood", weight=3];
1499[label="vz12000/Zero",fontsize=10,color="white",style="solid",shape="box"];1349 -> 1499[label="",style="solid", color="burlywood", weight=9];
1499 -> 1398[label="",style="solid", color="burlywood", weight=3];
1350[label="primCmpInt (Neg vz12000) vz1190",fontsize=16,color="burlywood",shape="box"];1500[label="vz12000/Succ vz120000",fontsize=10,color="white",style="solid",shape="box"];1350 -> 1500[label="",style="solid", color="burlywood", weight=9];
1500 -> 1399[label="",style="solid", color="burlywood", weight=3];
1501[label="vz12000/Zero",fontsize=10,color="white",style="solid",shape="box"];1350 -> 1501[label="",style="solid", color="burlywood", weight=9];
1501 -> 1400[label="",style="solid", color="burlywood", weight=3];
1351[label="vz128 : merge compare vz129 (vz127 : vz130)\n  Ord a",fontsize=16,color="green",shape="box"];1351 -> 1401[label="",style="dashed", color="green", weight=3];
1352[label="vz128 : merge compare vz129 (vz127 : vz130)\n  Ord a",fontsize=16,color="green",shape="box"];1352 -> 1402[label="",style="dashed", color="green", weight=3];
1353[label="vz127 : merge compare (vz128 : vz129) vz130\n  Ord a",fontsize=16,color="green",shape="box"];1353 -> 1403[label="",style="dashed", color="green", weight=3];
1239[label="merge compare vz117 (merge compare vz1180 (vz118100 : vz118101))\n  Ord a",fontsize=16,color="burlywood",shape="box"];1502[label="vz1180/vz11800 : vz11801",fontsize=10,color="white",style="solid",shape="box"];1239 -> 1502[label="",style="solid", color="burlywood", weight=9];
1502 -> 1253[label="",style="solid", color="burlywood", weight=3];
1503[label="vz1180/[]",fontsize=10,color="white",style="solid",shape="box"];1239 -> 1503[label="",style="solid", color="burlywood", weight=9];
1503 -> 1254[label="",style="solid", color="burlywood", weight=3];
1240[label="merge compare vz117 (merge compare vz1180 [])\n  Ord a",fontsize=16,color="black",shape="box"];1240 -> 1255[label="",style="solid", color="black", weight=3];
1241[label="merge_pairs compare (vz118110 : vz118111)\n  Ord a",fontsize=16,color="burlywood",shape="box"];1504[label="vz118111/vz1181110 : vz1181111",fontsize=10,color="white",style="solid",shape="box"];1241 -> 1504[label="",style="solid", color="burlywood", weight=9];
1504 -> 1256[label="",style="solid", color="burlywood", weight=3];
1505[label="vz118111/[]",fontsize=10,color="white",style="solid",shape="box"];1241 -> 1505[label="",style="solid", color="burlywood", weight=9];
1505 -> 1257[label="",style="solid", color="burlywood", weight=3];
1242[label="merge_pairs compare []\n  Ord a",fontsize=16,color="black",shape="box"];1242 -> 1258[label="",style="solid", color="black", weight=3];
1243[label="merge compare vz117 (vz11800 : vz11801)\n  Ord a",fontsize=16,color="burlywood",shape="box"];1506[label="vz117/vz1170 : vz1171",fontsize=10,color="white",style="solid",shape="box"];1243 -> 1506[label="",style="solid", color="burlywood", weight=9];
1506 -> 1259[label="",style="solid", color="burlywood", weight=3];
1507[label="vz117/[]",fontsize=10,color="white",style="solid",shape="box"];1243 -> 1507[label="",style="solid", color="burlywood", weight=9];
1507 -> 1260[label="",style="solid", color="burlywood", weight=3];
1244[label="merge compare vz117 []\n  Ord a",fontsize=16,color="black",shape="box"];1244 -> 1261[label="",style="solid", color="black", weight=3];
1397[label="primCmpInt (Pos (Succ vz120000)) vz1190",fontsize=16,color="burlywood",shape="box"];1508[label="vz1190/Pos vz11900",fontsize=10,color="white",style="solid",shape="box"];1397 -> 1508[label="",style="solid", color="burlywood", weight=9];
1508 -> 1404[label="",style="solid", color="burlywood", weight=3];
1509[label="vz1190/Neg vz11900",fontsize=10,color="white",style="solid",shape="box"];1397 -> 1509[label="",style="solid", color="burlywood", weight=9];
1509 -> 1405[label="",style="solid", color="burlywood", weight=3];
1398[label="primCmpInt (Pos Zero) vz1190",fontsize=16,color="burlywood",shape="box"];1510[label="vz1190/Pos vz11900",fontsize=10,color="white",style="solid",shape="box"];1398 -> 1510[label="",style="solid", color="burlywood", weight=9];
1510 -> 1406[label="",style="solid", color="burlywood", weight=3];
1511[label="vz1190/Neg vz11900",fontsize=10,color="white",style="solid",shape="box"];1398 -> 1511[label="",style="solid", color="burlywood", weight=9];
1511 -> 1407[label="",style="solid", color="burlywood", weight=3];
1399[label="primCmpInt (Neg (Succ vz120000)) vz1190",fontsize=16,color="burlywood",shape="box"];1512[label="vz1190/Pos vz11900",fontsize=10,color="white",style="solid",shape="box"];1399 -> 1512[label="",style="solid", color="burlywood", weight=9];
1512 -> 1408[label="",style="solid", color="burlywood", weight=3];
1513[label="vz1190/Neg vz11900",fontsize=10,color="white",style="solid",shape="box"];1399 -> 1513[label="",style="solid", color="burlywood", weight=9];
1513 -> 1409[label="",style="solid", color="burlywood", weight=3];
1400[label="primCmpInt (Neg Zero) vz1190",fontsize=16,color="burlywood",shape="box"];1514[label="vz1190/Pos vz11900",fontsize=10,color="white",style="solid",shape="box"];1400 -> 1514[label="",style="solid", color="burlywood", weight=9];
1514 -> 1410[label="",style="solid", color="burlywood", weight=3];
1515[label="vz1190/Neg vz11900",fontsize=10,color="white",style="solid",shape="box"];1400 -> 1515[label="",style="solid", color="burlywood", weight=9];
1515 -> 1411[label="",style="solid", color="burlywood", weight=3];
1401 -> 1233[label="",style="dashed", color="red", weight=0];
1401[label="merge compare vz129 (vz127 : vz130)\n  Ord a",fontsize=16,color="magenta"];1401 -> 1412[label="",style="dashed", color="magenta", weight=3];
1401 -> 1413[label="",style="dashed", color="magenta", weight=3];
1402 -> 1233[label="",style="dashed", color="red", weight=0];
1402[label="merge compare vz129 (vz127 : vz130)\n  Ord a",fontsize=16,color="magenta"];1402 -> 1414[label="",style="dashed", color="magenta", weight=3];
1402 -> 1415[label="",style="dashed", color="magenta", weight=3];
1403 -> 1233[label="",style="dashed", color="red", weight=0];
1403[label="merge compare (vz128 : vz129) vz130\n  Ord a",fontsize=16,color="magenta"];1403 -> 1416[label="",style="dashed", color="magenta", weight=3];
1403 -> 1417[label="",style="dashed", color="magenta", weight=3];
1253[label="merge compare vz117 (merge compare (vz11800 : vz11801) (vz118100 : vz118101))\n  Ord a",fontsize=16,color="black",shape="box"];1253 -> 1274[label="",style="solid", color="black", weight=3];
1254[label="merge compare vz117 (merge compare [] (vz118100 : vz118101))\n  Ord a",fontsize=16,color="black",shape="box"];1254 -> 1275[label="",style="solid", color="black", weight=3];
1255 -> 1233[label="",style="dashed", color="red", weight=0];
1255[label="merge compare vz117 vz1180\n  Ord a",fontsize=16,color="magenta"];1256[label="merge_pairs compare (vz118110 : vz1181110 : vz1181111)\n  Ord a",fontsize=16,color="black",shape="box"];1256 -> 1276[label="",style="solid", color="black", weight=3];
1257[label="merge_pairs compare (vz118110 : [])\n  Ord a",fontsize=16,color="black",shape="box"];1257 -> 1277[label="",style="solid", color="black", weight=3];
1258[label="[]\n  Ord a",fontsize=16,color="green",shape="box"];1259[label="merge compare (vz1170 : vz1171) (vz11800 : vz11801)\n  Ord a",fontsize=16,color="black",shape="box"];1259 -> 1278[label="",style="solid", color="black", weight=3];
1260[label="merge compare [] (vz11800 : vz11801)\n  Ord a",fontsize=16,color="black",shape="box"];1260 -> 1279[label="",style="solid", color="black", weight=3];
1261[label="vz117\n  Ord a",fontsize=16,color="green",shape="box"];1404[label="primCmpInt (Pos (Succ vz120000)) (Pos vz11900)",fontsize=16,color="black",shape="box"];1404 -> 1418[label="",style="solid", color="black", weight=3];
1405[label="primCmpInt (Pos (Succ vz120000)) (Neg vz11900)",fontsize=16,color="black",shape="box"];1405 -> 1419[label="",style="solid", color="black", weight=3];
1406[label="primCmpInt (Pos Zero) (Pos vz11900)",fontsize=16,color="burlywood",shape="box"];1520[label="vz11900/Succ vz119000",fontsize=10,color="white",style="solid",shape="box"];1406 -> 1520[label="",style="solid", color="burlywood", weight=9];
1520 -> 1420[label="",style="solid", color="burlywood", weight=3];
1521[label="vz11900/Zero",fontsize=10,color="white",style="solid",shape="box"];1406 -> 1521[label="",style="solid", color="burlywood", weight=9];
1521 -> 1421[label="",style="solid", color="burlywood", weight=3];
1407[label="primCmpInt (Pos Zero) (Neg vz11900)",fontsize=16,color="burlywood",shape="box"];1522[label="vz11900/Succ vz119000",fontsize=10,color="white",style="solid",shape="box"];1407 -> 1522[label="",style="solid", color="burlywood", weight=9];
1522 -> 1422[label="",style="solid", color="burlywood", weight=3];
1523[label="vz11900/Zero",fontsize=10,color="white",style="solid",shape="box"];1407 -> 1523[label="",style="solid", color="burlywood", weight=9];
1523 -> 1423[label="",style="solid", color="burlywood", weight=3];
1408[label="primCmpInt (Neg (Succ vz120000)) (Pos vz11900)",fontsize=16,color="black",shape="box"];1408 -> 1424[label="",style="solid", color="black", weight=3];
1409[label="primCmpInt (Neg (Succ vz120000)) (Neg vz11900)",fontsize=16,color="black",shape="box"];1409 -> 1425[label="",style="solid", color="black", weight=3];
1410[label="primCmpInt (Neg Zero) (Pos vz11900)",fontsize=16,color="burlywood",shape="box"];1524[label="vz11900/Succ vz119000",fontsize=10,color="white",style="solid",shape="box"];1410 -> 1524[label="",style="solid", color="burlywood", weight=9];
1524 -> 1426[label="",style="solid", color="burlywood", weight=3];
1525[label="vz11900/Zero",fontsize=10,color="white",style="solid",shape="box"];1410 -> 1525[label="",style="solid", color="burlywood", weight=9];
1525 -> 1427[label="",style="solid", color="burlywood", weight=3];
1411[label="primCmpInt (Neg Zero) (Neg vz11900)",fontsize=16,color="burlywood",shape="box"];1526[label="vz11900/Succ vz119000",fontsize=10,color="white",style="solid",shape="box"];1411 -> 1526[label="",style="solid", color="burlywood", weight=9];
1526 -> 1428[label="",style="solid", color="burlywood", weight=3];
1527[label="vz11900/Zero",fontsize=10,color="white",style="solid",shape="box"];1411 -> 1527[label="",style="solid", color="burlywood", weight=9];
1527 -> 1429[label="",style="solid", color="burlywood", weight=3];
1412[label="vz127 : vz130\n  Ord a",fontsize=16,color="green",shape="box"];1413[label="vz129\n  Ord a",fontsize=16,color="green",shape="box"];1414[label="vz127 : vz130\n  Ord a",fontsize=16,color="green",shape="box"];1415[label="vz129\n  Ord a",fontsize=16,color="green",shape="box"];1416[label="vz130\n  Ord a",fontsize=16,color="green",shape="box"];1417[label="vz128 : vz129\n  Ord a",fontsize=16,color="green",shape="box"];1274 -> 1233[label="",style="dashed", color="red", weight=0];
1274[label="merge compare vz117 (merge0 vz118100 compare vz11800 vz11801 vz118101 (compare vz11800 vz118100))\n  Ord a",fontsize=16,color="magenta"];1274 -> 1294[label="",style="dashed", color="magenta", weight=3];
1275 -> 1233[label="",style="dashed", color="red", weight=0];
1275[label="merge compare vz117 (vz118100 : vz118101)\n  Ord a",fontsize=16,color="magenta"];1275 -> 1295[label="",style="dashed", color="magenta", weight=3];
1276[label="merge compare vz118110 vz1181110 : merge_pairs compare vz1181111\n  Ord a",fontsize=16,color="green",shape="box"];1276 -> 1296[label="",style="dashed", color="green", weight=3];
1276 -> 1297[label="",style="dashed", color="green", weight=3];
1277[label="vz118110 : []\n  Ord a",fontsize=16,color="green",shape="box"];1278 -> 1298[label="",style="dashed", color="red", weight=0];
1278[label="merge0 vz11800 compare vz1170 vz1171 vz11801 (compare vz1170 vz11800)\n  Ord a",fontsize=16,color="magenta"];1278 -> 1304[label="",style="dashed", color="magenta", weight=3];
1278 -> 1305[label="",style="dashed", color="magenta", weight=3];
1278 -> 1306[label="",style="dashed", color="magenta", weight=3];
1278 -> 1307[label="",style="dashed", color="magenta", weight=3];
1278 -> 1308[label="",style="dashed", color="magenta", weight=3];
1279[label="vz11800 : vz11801\n  Ord a",fontsize=16,color="green",shape="box"];1418[label="primCmpNat (Succ vz120000) vz11900",fontsize=16,color="burlywood",shape="triangle"];1531[label="vz11900/Succ vz119000",fontsize=10,color="white",style="solid",shape="box"];1418 -> 1531[label="",style="solid", color="burlywood", weight=9];
1531 -> 1430[label="",style="solid", color="burlywood", weight=3];
1532[label="vz11900/Zero",fontsize=10,color="white",style="solid",shape="box"];1418 -> 1532[label="",style="solid", color="burlywood", weight=9];
1532 -> 1431[label="",style="solid", color="burlywood", weight=3];
1419[label="GT",fontsize=16,color="green",shape="box"];1420[label="primCmpInt (Pos Zero) (Pos (Succ vz119000))",fontsize=16,color="black",shape="box"];1420 -> 1432[label="",style="solid", color="black", weight=3];
1421[label="primCmpInt (Pos Zero) (Pos Zero)",fontsize=16,color="black",shape="box"];1421 -> 1433[label="",style="solid", color="black", weight=3];
1422[label="primCmpInt (Pos Zero) (Neg (Succ vz119000))",fontsize=16,color="black",shape="box"];1422 -> 1434[label="",style="solid", color="black", weight=3];
1423[label="primCmpInt (Pos Zero) (Neg Zero)",fontsize=16,color="black",shape="box"];1423 -> 1435[label="",style="solid", color="black", weight=3];
1424[label="LT",fontsize=16,color="green",shape="box"];1425[label="primCmpNat vz11900 (Succ vz120000)",fontsize=16,color="burlywood",shape="triangle"];1533[label="vz11900/Succ vz119000",fontsize=10,color="white",style="solid",shape="box"];1425 -> 1533[label="",style="solid", color="burlywood", weight=9];
1533 -> 1436[label="",style="solid", color="burlywood", weight=3];
1534[label="vz11900/Zero",fontsize=10,color="white",style="solid",shape="box"];1425 -> 1534[label="",style="solid", color="burlywood", weight=9];
1534 -> 1437[label="",style="solid", color="burlywood", weight=3];
1426[label="primCmpInt (Neg Zero) (Pos (Succ vz119000))",fontsize=16,color="black",shape="box"];1426 -> 1438[label="",style="solid", color="black", weight=3];
1427[label="primCmpInt (Neg Zero) (Pos Zero)",fontsize=16,color="black",shape="box"];1427 -> 1439[label="",style="solid", color="black", weight=3];
1428[label="primCmpInt (Neg Zero) (Neg (Succ vz119000))",fontsize=16,color="black",shape="box"];1428 -> 1440[label="",style="solid", color="black", weight=3];
1429[label="primCmpInt (Neg Zero) (Neg Zero)",fontsize=16,color="black",shape="box"];1429 -> 1441[label="",style="solid", color="black", weight=3];
1294 -> 1298[label="",style="dashed", color="red", weight=0];
1294[label="merge0 vz118100 compare vz11800 vz11801 vz118101 (compare vz11800 vz118100)\n  Ord a",fontsize=16,color="magenta"];1294 -> 1309[label="",style="dashed", color="magenta", weight=3];
1294 -> 1310[label="",style="dashed", color="magenta", weight=3];
1294 -> 1311[label="",style="dashed", color="magenta", weight=3];
1294 -> 1312[label="",style="dashed", color="magenta", weight=3];
1294 -> 1313[label="",style="dashed", color="magenta", weight=3];
1295[label="vz118100 : vz118101\n  Ord a",fontsize=16,color="green",shape="box"];1296 -> 1233[label="",style="dashed", color="red", weight=0];
1296[label="merge compare vz118110 vz1181110\n  Ord a",fontsize=16,color="magenta"];1296 -> 1318[label="",style="dashed", color="magenta", weight=3];
1296 -> 1319[label="",style="dashed", color="magenta", weight=3];
1297 -> 1232[label="",style="dashed", color="red", weight=0];
1297[label="merge_pairs compare vz1181111\n  Ord a",fontsize=16,color="magenta"];1297 -> 1320[label="",style="dashed", color="magenta", weight=3];
1304[label="vz11801\n  Ord a",fontsize=16,color="green",shape="box"];1305[label="vz1171\n  Ord a",fontsize=16,color="green",shape="box"];1306[label="vz1170\n  Ord a",fontsize=16,color="green",shape="box"];1307[label="vz11800\n  Ord a",fontsize=16,color="green",shape="box"];1308[label="compare vz1170 vz11800\n  Ord a",fontsize=16,color="blue",shape="box"];1538[label="compare :: Float -> Float -> Ordering",fontsize=10,color="white",style="solid",shape="box"];1308 -> 1538[label="",style="solid", color="blue", weight=9];
1538 -> 1321[label="",style="solid", color="blue", weight=3];
1539[label="compare :: ((@2) a b) -> ((@2) a b) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];1308 -> 1539[label="",style="solid", color="blue", weight=9];
1539 -> 1322[label="",style="solid", color="blue", weight=3];
1540[label="compare :: (Ratio a) -> (Ratio a) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];1308 -> 1540[label="",style="solid", color="blue", weight=9];
1540 -> 1323[label="",style="solid", color="blue", weight=3];
1541[label="compare :: ([] a) -> ([] a) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];1308 -> 1541[label="",style="solid", color="blue", weight=9];
1541 -> 1324[label="",style="solid", color="blue", weight=3];
1542[label="compare :: ((@3) a b c) -> ((@3) a b c) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];1308 -> 1542[label="",style="solid", color="blue", weight=9];
1542 -> 1325[label="",style="solid", color="blue", weight=3];
1543[label="compare :: (Either a b) -> (Either a b) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];1308 -> 1543[label="",style="solid", color="blue", weight=9];
1543 -> 1326[label="",style="solid", color="blue", weight=3];
1544[label="compare :: Double -> Double -> Ordering",fontsize=10,color="white",style="solid",shape="box"];1308 -> 1544[label="",style="solid", color="blue", weight=9];
1544 -> 1327[label="",style="solid", color="blue", weight=3];
1545[label="compare :: Int -> Int -> Ordering",fontsize=10,color="white",style="solid",shape="box"];1308 -> 1545[label="",style="solid", color="blue", weight=9];
1545 -> 1328[label="",style="solid", color="blue", weight=3];
1546[label="compare :: Ordering -> Ordering -> Ordering",fontsize=10,color="white",style="solid",shape="box"];1308 -> 1546[label="",style="solid", color="blue", weight=9];
1546 -> 1329[label="",style="solid", color="blue", weight=3];
1547[label="compare :: Bool -> Bool -> Ordering",fontsize=10,color="white",style="solid",shape="box"];1308 -> 1547[label="",style="solid", color="blue", weight=9];
1547 -> 1330[label="",style="solid", color="blue", weight=3];
1548[label="compare :: (Maybe a) -> (Maybe a) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];1308 -> 1548[label="",style="solid", color="blue", weight=9];
1548 -> 1331[label="",style="solid", color="blue", weight=3];
1549[label="compare :: Char -> Char -> Ordering",fontsize=10,color="white",style="solid",shape="box"];1308 -> 1549[label="",style="solid", color="blue", weight=9];
1549 -> 1332[label="",style="solid", color="blue", weight=3];
1550[label="compare :: Integer -> Integer -> Ordering",fontsize=10,color="white",style="solid",shape="box"];1308 -> 1550[label="",style="solid", color="blue", weight=9];
1550 -> 1333[label="",style="solid", color="blue", weight=3];
1551[label="compare :: () -> () -> Ordering",fontsize=10,color="white",style="solid",shape="box"];1308 -> 1551[label="",style="solid", color="blue", weight=9];
1551 -> 1334[label="",style="solid", color="blue", weight=3];
1430[label="primCmpNat (Succ vz120000) (Succ vz119000)",fontsize=16,color="black",shape="box"];1430 -> 1442[label="",style="solid", color="black", weight=3];
1431[label="primCmpNat (Succ vz120000) Zero",fontsize=16,color="black",shape="box"];1431 -> 1443[label="",style="solid", color="black", weight=3];
1432 -> 1425[label="",style="dashed", color="red", weight=0];
1432[label="primCmpNat Zero (Succ vz119000)",fontsize=16,color="magenta"];1432 -> 1444[label="",style="dashed", color="magenta", weight=3];
1432 -> 1445[label="",style="dashed", color="magenta", weight=3];
1433[label="EQ",fontsize=16,color="green",shape="box"];1434[label="GT",fontsize=16,color="green",shape="box"];1435[label="EQ",fontsize=16,color="green",shape="box"];1436[label="primCmpNat (Succ vz119000) (Succ vz120000)",fontsize=16,color="black",shape="box"];1436 -> 1446[label="",style="solid", color="black", weight=3];
1437[label="primCmpNat Zero (Succ vz120000)",fontsize=16,color="black",shape="box"];1437 -> 1447[label="",style="solid", color="black", weight=3];
1438[label="LT",fontsize=16,color="green",shape="box"];1439[label="EQ",fontsize=16,color="green",shape="box"];1440 -> 1418[label="",style="dashed", color="red", weight=0];
1440[label="primCmpNat (Succ vz119000) Zero",fontsize=16,color="magenta"];1440 -> 1448[label="",style="dashed", color="magenta", weight=3];
1440 -> 1449[label="",style="dashed", color="magenta", weight=3];
1441[label="EQ",fontsize=16,color="green",shape="box"];1309[label="vz118101\n  Ord a",fontsize=16,color="green",shape="box"];1310[label="vz11801\n  Ord a",fontsize=16,color="green",shape="box"];1311[label="vz11800\n  Ord a",fontsize=16,color="green",shape="box"];1312[label="vz118100\n  Ord a",fontsize=16,color="green",shape="box"];1313[label="compare vz11800 vz118100\n  Ord a",fontsize=16,color="blue",shape="box"];1554[label="compare :: Float -> Float -> Ordering",fontsize=10,color="white",style="solid",shape="box"];1313 -> 1554[label="",style="solid", color="blue", weight=9];
1554 -> 1335[label="",style="solid", color="blue", weight=3];
1555[label="compare :: ((@2) a b) -> ((@2) a b) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];1313 -> 1555[label="",style="solid", color="blue", weight=9];
1555 -> 1336[label="",style="solid", color="blue", weight=3];
1556[label="compare :: (Ratio a) -> (Ratio a) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];1313 -> 1556[label="",style="solid", color="blue", weight=9];
1556 -> 1337[label="",style="solid", color="blue", weight=3];
1557[label="compare :: ([] a) -> ([] a) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];1313 -> 1557[label="",style="solid", color="blue", weight=9];
1557 -> 1338[label="",style="solid", color="blue", weight=3];
1558[label="compare :: ((@3) a b c) -> ((@3) a b c) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];1313 -> 1558[label="",style="solid", color="blue", weight=9];
1558 -> 1339[label="",style="solid", color="blue", weight=3];
1559[label="compare :: (Either a b) -> (Either a b) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];1313 -> 1559[label="",style="solid", color="blue", weight=9];
1559 -> 1340[label="",style="solid", color="blue", weight=3];
1560[label="compare :: Double -> Double -> Ordering",fontsize=10,color="white",style="solid",shape="box"];1313 -> 1560[label="",style="solid", color="blue", weight=9];
1560 -> 1341[label="",style="solid", color="blue", weight=3];
1561[label="compare :: Int -> Int -> Ordering",fontsize=10,color="white",style="solid",shape="box"];1313 -> 1561[label="",style="solid", color="blue", weight=9];
1561 -> 1342[label="",style="solid", color="blue", weight=3];
1562[label="compare :: Ordering -> Ordering -> Ordering",fontsize=10,color="white",style="solid",shape="box"];1313 -> 1562[label="",style="solid", color="blue", weight=9];
1562 -> 1343[label="",style="solid", color="blue", weight=3];
1563[label="compare :: Bool -> Bool -> Ordering",fontsize=10,color="white",style="solid",shape="box"];1313 -> 1563[label="",style="solid", color="blue", weight=9];
1563 -> 1344[label="",style="solid", color="blue", weight=3];
1564[label="compare :: (Maybe a) -> (Maybe a) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];1313 -> 1564[label="",style="solid", color="blue", weight=9];
1564 -> 1345[label="",style="solid", color="blue", weight=3];
1565[label="compare :: Char -> Char -> Ordering",fontsize=10,color="white",style="solid",shape="box"];1313 -> 1565[label="",style="solid", color="blue", weight=9];
1565 -> 1346[label="",style="solid", color="blue", weight=3];
1566[label="compare :: Integer -> Integer -> Ordering",fontsize=10,color="white",style="solid",shape="box"];1313 -> 1566[label="",style="solid", color="blue", weight=9];
1566 -> 1347[label="",style="solid", color="blue", weight=3];
1567[label="compare :: () -> () -> Ordering",fontsize=10,color="white",style="solid",shape="box"];1313 -> 1567[label="",style="solid", color="blue", weight=9];
1567 -> 1348[label="",style="solid", color="blue", weight=3];
1318[label="vz1181110\n  Ord a",fontsize=16,color="green",shape="box"];1319[label="vz118110\n  Ord a",fontsize=16,color="green",shape="box"];1320[label="vz1181111\n  Ord a",fontsize=16,color="green",shape="box"];1321[label="compare vz1170 vz11800",fontsize=16,color="black",shape="triangle"];1321 -> 1354[label="",style="solid", color="black", weight=3];
1322[label="compare vz1170 vz11800\n  Ord a  Ord b",fontsize=16,color="black",shape="triangle"];1322 -> 1355[label="",style="solid", color="black", weight=3];
1323[label="compare vz1170 vz11800\n  Integral a",fontsize=16,color="black",shape="triangle"];1323 -> 1356[label="",style="solid", color="black", weight=3];
1324[label="compare vz1170 vz11800\n  Ord a",fontsize=16,color="black",shape="triangle"];1324 -> 1357[label="",style="solid", color="black", weight=3];
1325[label="compare vz1170 vz11800\n  Ord a  Ord b  Ord c",fontsize=16,color="black",shape="triangle"];1325 -> 1358[label="",style="solid", color="black", weight=3];
1326[label="compare vz1170 vz11800\n  Ord a  Ord b",fontsize=16,color="black",shape="triangle"];1326 -> 1359[label="",style="solid", color="black", weight=3];
1327[label="compare vz1170 vz11800",fontsize=16,color="black",shape="triangle"];1327 -> 1360[label="",style="solid", color="black", weight=3];
1328 -> 1303[label="",style="dashed", color="red", weight=0];
1328[label="compare vz1170 vz11800",fontsize=16,color="magenta"];1328 -> 1361[label="",style="dashed", color="magenta", weight=3];
1328 -> 1362[label="",style="dashed", color="magenta", weight=3];
1329[label="compare vz1170 vz11800",fontsize=16,color="black",shape="triangle"];1329 -> 1363[label="",style="solid", color="black", weight=3];
1330[label="compare vz1170 vz11800",fontsize=16,color="black",shape="triangle"];1330 -> 1364[label="",style="solid", color="black", weight=3];
1331[label="compare vz1170 vz11800\n  Ord a",fontsize=16,color="black",shape="triangle"];1331 -> 1365[label="",style="solid", color="black", weight=3];
1332[label="compare vz1170 vz11800",fontsize=16,color="black",shape="triangle"];1332 -> 1366[label="",style="solid", color="black", weight=3];
1333[label="compare vz1170 vz11800",fontsize=16,color="black",shape="triangle"];1333 -> 1367[label="",style="solid", color="black", weight=3];
1334[label="compare vz1170 vz11800",fontsize=16,color="black",shape="triangle"];1334 -> 1368[label="",style="solid", color="black", weight=3];
1442[label="primCmpNat vz120000 vz119000",fontsize=16,color="burlywood",shape="triangle"];1569[label="vz120000/Succ vz1200000",fontsize=10,color="white",style="solid",shape="box"];1442 -> 1569[label="",style="solid", color="burlywood", weight=9];
1569 -> 1450[label="",style="solid", color="burlywood", weight=3];
1570[label="vz120000/Zero",fontsize=10,color="white",style="solid",shape="box"];1442 -> 1570[label="",style="solid", color="burlywood", weight=9];
1570 -> 1451[label="",style="solid", color="burlywood", weight=3];
1443[label="GT",fontsize=16,color="green",shape="box"];1444[label="vz119000",fontsize=16,color="green",shape="box"];1445[label="Zero",fontsize=16,color="green",shape="box"];1446 -> 1442[label="",style="dashed", color="red", weight=0];
1446[label="primCmpNat vz119000 vz120000",fontsize=16,color="magenta"];1446 -> 1452[label="",style="dashed", color="magenta", weight=3];
1446 -> 1453[label="",style="dashed", color="magenta", weight=3];
1447[label="LT",fontsize=16,color="green",shape="box"];1448[label="vz119000",fontsize=16,color="green",shape="box"];1449[label="Zero",fontsize=16,color="green",shape="box"];1335 -> 1321[label="",style="dashed", color="red", weight=0];
1335[label="compare vz11800 vz118100",fontsize=16,color="magenta"];1335 -> 1369[label="",style="dashed", color="magenta", weight=3];
1335 -> 1370[label="",style="dashed", color="magenta", weight=3];
1336 -> 1322[label="",style="dashed", color="red", weight=0];
1336[label="compare vz11800 vz118100\n  Ord a  Ord b",fontsize=16,color="magenta"];1336 -> 1371[label="",style="dashed", color="magenta", weight=3];
1336 -> 1372[label="",style="dashed", color="magenta", weight=3];
1337 -> 1323[label="",style="dashed", color="red", weight=0];
1337[label="compare vz11800 vz118100\n  Integral a",fontsize=16,color="magenta"];1337 -> 1373[label="",style="dashed", color="magenta", weight=3];
1337 -> 1374[label="",style="dashed", color="magenta", weight=3];
1338 -> 1324[label="",style="dashed", color="red", weight=0];
1338[label="compare vz11800 vz118100\n  Ord a",fontsize=16,color="magenta"];1338 -> 1375[label="",style="dashed", color="magenta", weight=3];
1338 -> 1376[label="",style="dashed", color="magenta", weight=3];
1339 -> 1325[label="",style="dashed", color="red", weight=0];
1339[label="compare vz11800 vz118100\n  Ord a  Ord b  Ord c",fontsize=16,color="magenta"];1339 -> 1377[label="",style="dashed", color="magenta", weight=3];
1339 -> 1378[label="",style="dashed", color="magenta", weight=3];
1340 -> 1326[label="",style="dashed", color="red", weight=0];
1340[label="compare vz11800 vz118100\n  Ord a  Ord b",fontsize=16,color="magenta"];1340 -> 1379[label="",style="dashed", color="magenta", weight=3];
1340 -> 1380[label="",style="dashed", color="magenta", weight=3];
1341 -> 1327[label="",style="dashed", color="red", weight=0];
1341[label="compare vz11800 vz118100",fontsize=16,color="magenta"];1341 -> 1381[label="",style="dashed", color="magenta", weight=3];
1341 -> 1382[label="",style="dashed", color="magenta", weight=3];
1342 -> 1303[label="",style="dashed", color="red", weight=0];
1342[label="compare vz11800 vz118100",fontsize=16,color="magenta"];1342 -> 1383[label="",style="dashed", color="magenta", weight=3];
1342 -> 1384[label="",style="dashed", color="magenta", weight=3];
1343 -> 1329[label="",style="dashed", color="red", weight=0];
1343[label="compare vz11800 vz118100",fontsize=16,color="magenta"];1343 -> 1385[label="",style="dashed", color="magenta", weight=3];
1343 -> 1386[label="",style="dashed", color="magenta", weight=3];
1344 -> 1330[label="",style="dashed", color="red", weight=0];
1344[label="compare vz11800 vz118100",fontsize=16,color="magenta"];1344 -> 1387[label="",style="dashed", color="magenta", weight=3];
1344 -> 1388[label="",style="dashed", color="magenta", weight=3];
1345 -> 1331[label="",style="dashed", color="red", weight=0];
1345[label="compare vz11800 vz118100\n  Ord a",fontsize=16,color="magenta"];1345 -> 1389[label="",style="dashed", color="magenta", weight=3];
1345 -> 1390[label="",style="dashed", color="magenta", weight=3];
1346 -> 1332[label="",style="dashed", color="red", weight=0];
1346[label="compare vz11800 vz118100",fontsize=16,color="magenta"];1346 -> 1391[label="",style="dashed", color="magenta", weight=3];
1346 -> 1392[label="",style="dashed", color="magenta", weight=3];
1347 -> 1333[label="",style="dashed", color="red", weight=0];
1347[label="compare vz11800 vz118100",fontsize=16,color="magenta"];1347 -> 1393[label="",style="dashed", color="magenta", weight=3];
1347 -> 1394[label="",style="dashed", color="magenta", weight=3];
1348 -> 1334[label="",style="dashed", color="red", weight=0];
1348[label="compare vz11800 vz118100",fontsize=16,color="magenta"];1348 -> 1395[label="",style="dashed", color="magenta", weight=3];
1348 -> 1396[label="",style="dashed", color="magenta", weight=3];
1354[label="error []",fontsize=16,color="red",shape="box"];1355[label="error []",fontsize=16,color="red",shape="box"];1356[label="error []",fontsize=16,color="red",shape="box"];1357[label="error []",fontsize=16,color="red",shape="box"];1358[label="error []",fontsize=16,color="red",shape="box"];1359[label="error []",fontsize=16,color="red",shape="box"];1360[label="error []",fontsize=16,color="red",shape="box"];1361[label="vz1170",fontsize=16,color="green",shape="box"];1362[label="vz11800",fontsize=16,color="green",shape="box"];1363[label="error []",fontsize=16,color="red",shape="box"];1364[label="error []",fontsize=16,color="red",shape="box"];1365[label="error []",fontsize=16,color="red",shape="box"];1366[label="error []",fontsize=16,color="red",shape="box"];1367[label="error []",fontsize=16,color="red",shape="box"];1368[label="error []",fontsize=16,color="red",shape="box"];1450[label="primCmpNat (Succ vz1200000) vz119000",fontsize=16,color="burlywood",shape="box"];1586[label="vz119000/Succ vz1190000",fontsize=10,color="white",style="solid",shape="box"];1450 -> 1586[label="",style="solid", color="burlywood", weight=9];
1586 -> 1454[label="",style="solid", color="burlywood", weight=3];
1587[label="vz119000/Zero",fontsize=10,color="white",style="solid",shape="box"];1450 -> 1587[label="",style="solid", color="burlywood", weight=9];
1587 -> 1455[label="",style="solid", color="burlywood", weight=3];
1451[label="primCmpNat Zero vz119000",fontsize=16,color="burlywood",shape="box"];1588[label="vz119000/Succ vz1190000",fontsize=10,color="white",style="solid",shape="box"];1451 -> 1588[label="",style="solid", color="burlywood", weight=9];
1588 -> 1456[label="",style="solid", color="burlywood", weight=3];
1589[label="vz119000/Zero",fontsize=10,color="white",style="solid",shape="box"];1451 -> 1589[label="",style="solid", color="burlywood", weight=9];
1589 -> 1457[label="",style="solid", color="burlywood", weight=3];
1452[label="vz120000",fontsize=16,color="green",shape="box"];1453[label="vz119000",fontsize=16,color="green",shape="box"];1369[label="vz11800",fontsize=16,color="green",shape="box"];1370[label="vz118100",fontsize=16,color="green",shape="box"];1371[label="vz11800\n  Ord a  Ord b",fontsize=16,color="green",shape="box"];1372[label="vz118100\n  Ord a  Ord b",fontsize=16,color="green",shape="box"];1373[label="vz11800\n  Integral a",fontsize=16,color="green",shape="box"];1374[label="vz118100\n  Integral a",fontsize=16,color="green",shape="box"];1375[label="vz11800\n  Ord a",fontsize=16,color="green",shape="box"];1376[label="vz118100\n  Ord a",fontsize=16,color="green",shape="box"];1377[label="vz11800\n  Ord a  Ord b  Ord c",fontsize=16,color="green",shape="box"];1378[label="vz118100\n  Ord a  Ord b  Ord c",fontsize=16,color="green",shape="box"];1379[label="vz11800\n  Ord a  Ord b",fontsize=16,color="green",shape="box"];1380[label="vz118100\n  Ord a  Ord b",fontsize=16,color="green",shape="box"];1381[label="vz11800",fontsize=16,color="green",shape="box"];1382[label="vz118100",fontsize=16,color="green",shape="box"];1383[label="vz11800",fontsize=16,color="green",shape="box"];1384[label="vz118100",fontsize=16,color="green",shape="box"];1385[label="vz11800",fontsize=16,color="green",shape="box"];1386[label="vz118100",fontsize=16,color="green",shape="box"];1387[label="vz11800",fontsize=16,color="green",shape="box"];1388[label="vz118100",fontsize=16,color="green",shape="box"];1389[label="vz11800\n  Ord a",fontsize=16,color="green",shape="box"];1390[label="vz118100\n  Ord a",fontsize=16,color="green",shape="box"];1391[label="vz11800",fontsize=16,color="green",shape="box"];1392[label="vz118100",fontsize=16,color="green",shape="box"];1393[label="vz11800",fontsize=16,color="green",shape="box"];1394[label="vz118100",fontsize=16,color="green",shape="box"];1395[label="vz11800",fontsize=16,color="green",shape="box"];1396[label="vz118100",fontsize=16,color="green",shape="box"];1454[label="primCmpNat (Succ vz1200000) (Succ vz1190000)",fontsize=16,color="black",shape="box"];1454 -> 1458[label="",style="solid", color="black", weight=3];
1455[label="primCmpNat (Succ vz1200000) Zero",fontsize=16,color="black",shape="box"];1455 -> 1459[label="",style="solid", color="black", weight=3];
1456[label="primCmpNat Zero (Succ vz1190000)",fontsize=16,color="black",shape="box"];1456 -> 1460[label="",style="solid", color="black", weight=3];
1457[label="primCmpNat Zero Zero",fontsize=16,color="black",shape="box"];1457 -> 1461[label="",style="solid", color="black", weight=3];
1458 -> 1442[label="",style="dashed", color="red", weight=0];
1458[label="primCmpNat vz1200000 vz1190000",fontsize=16,color="magenta"];1458 -> 1462[label="",style="dashed", color="magenta", weight=3];
1458 -> 1463[label="",style="dashed", color="magenta", weight=3];
1459[label="GT",fontsize=16,color="green",shape="box"];1460[label="LT",fontsize=16,color="green",shape="box"];1461[label="EQ",fontsize=16,color="green",shape="box"];1462[label="vz1190000",fontsize=16,color="green",shape="box"];1463[label="vz1200000",fontsize=16,color="green",shape="box"];}

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_map(:(vz3110, vz3111)) → new_map(vz3111)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_map(:(vz3110, vz3111)) → new_map(vz3111)
The graph contains the following edges 1 > 1

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primCmpNat(Succ(vz1200000), Succ(vz1190000)) → new_primCmpNat(vz1200000, vz1190000)

From the DPs we obtained the following set of size-change graphs:

new_primCmpNat(Succ(vz1200000), Succ(vz1190000)) → new_primCmpNat(vz1200000, vz1190000)
The graph contains the following edges 1 > 1, 2 > 2

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPOrderProof

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_merge0(vz127, vz128, vz129, vz130, GT, ba) → new_merge(:(vz128, vz129), vz130, ba)
new_merge0(vz127, vz128, vz129, vz130, EQ, ba) → new_merge(vz129, :(vz127, vz130), ba)
new_merge(:(vz1170, vz1171), :(vz11800, vz11801), bb) → new_merge0(vz11800, vz1170, vz1171, vz11801, new_compare(vz1170, vz11800, bb), bb)
new_merge0(vz127, vz128, vz129, vz130, LT, ba) → new_merge(vz129, :(vz127, vz130), ba)

The TRS R consists of the following rules:

new_compare2(vz1170, vz11800, bc) → error([])
new_compare(vz1170, vz11800, ty_Int) → new_compare0(vz1170, vz11800)
new_compare3(vz1170, vz11800, bd, be, bf) → error([])
new_compare(vz1170, vz11800, app(ty_Ratio, bc)) → new_compare2(vz1170, vz11800, bc)
new_compare(vz1170, vz11800, app(ty_Maybe, cd)) → new_compare12(vz1170, vz11800, cd)
new_primCmpNat0(vz120000, Succ(vz119000)) → new_primCmpNat2(vz120000, vz119000)
new_compare(vz1170, vz11800, app(ty_[], cc)) → new_compare8(vz1170, vz11800, cc)
new_compare4(vz1170, vz11800) → error([])
new_compare7(vz1170, vz11800, ca, cb) → error([])
new_compare0(Neg(Zero), Pos(Succ(vz119000))) → LT
new_compare(vz1170, vz11800, ty_Bool) → new_compare11(vz1170, vz11800)
new_compare10(vz1170, vz11800) → error([])
new_compare(vz1170, vz11800, ty_Integer) → new_compare13(vz1170, vz11800)
new_compare(vz1170, vz11800, ty_Float) → new_compare4(vz1170, vz11800)
new_compare(vz1170, vz11800, ty_Char) → new_compare1(vz1170, vz11800)
new_compare0(Neg(Succ(vz120000)), Pos(vz11900)) → LT
new_compare0(Neg(Zero), Neg(Zero)) → EQ
new_compare(vz1170, vz11800, ty_@0) → new_compare5(vz1170, vz11800)
new_compare1(vz1170, vz11800) → error([])
new_primCmpNat2(Zero, Zero) → EQ
new_compare0(Pos(Succ(vz120000)), Pos(vz11900)) → new_primCmpNat0(vz120000, vz11900)
new_compare(vz1170, vz11800, ty_Double) → new_compare9(vz1170, vz11800)
new_compare(vz1170, vz11800, app(app(ty_Either, bg), bh)) → new_compare6(vz1170, vz11800, bg, bh)
new_compare8(vz1170, vz11800, cc) → error([])
new_primCmpNat2(Zero, Succ(vz1190000)) → LT
new_compare5(vz1170, vz11800) → error([])
new_compare11(vz1170, vz11800) → error([])
new_compare(vz1170, vz11800, app(app(app(ty_@3, bd), be), bf)) → new_compare3(vz1170, vz11800, bd, be, bf)
new_compare0(Pos(Zero), Pos(Succ(vz119000))) → new_primCmpNat1(Zero, vz119000)
new_compare(vz1170, vz11800, app(app(ty_@2, ca), cb)) → new_compare7(vz1170, vz11800, ca, cb)
new_compare12(vz1170, vz11800, cd) → error([])
new_compare9(vz1170, vz11800) → error([])
new_primCmpNat1(Succ(vz119000), vz120000) → new_primCmpNat2(vz119000, vz120000)
new_compare(vz1170, vz11800, ty_Ordering) → new_compare10(vz1170, vz11800)
new_primCmpNat2(Succ(vz1200000), Succ(vz1190000)) → new_primCmpNat2(vz1200000, vz1190000)
new_primCmpNat2(Succ(vz1200000), Zero) → GT
new_compare0(Pos(Zero), Neg(Zero)) → EQ
new_compare0(Neg(Zero), Pos(Zero)) → EQ
new_compare0(Neg(Zero), Neg(Succ(vz119000))) → new_primCmpNat0(vz119000, Zero)
new_compare0(Pos(Succ(vz120000)), Neg(vz11900)) → GT
new_compare0(Neg(Succ(vz120000)), Neg(vz11900)) → new_primCmpNat1(vz11900, vz120000)
new_primCmpNat1(Zero, vz120000) → LT
new_compare13(vz1170, vz11800) → error([])
new_compare0(Pos(Zero), Pos(Zero)) → EQ
new_compare6(vz1170, vz11800, bg, bh) → error([])
new_primCmpNat0(vz120000, Zero) → GT
new_compare0(Pos(Zero), Neg(Succ(vz119000))) → GT

The set Q consists of the following terms:

new_compare8(x0, x1, x2)
new_compare0(Neg(Succ(x0)), Neg(x1))
new_compare0(Pos(Zero), Neg(Succ(x0)))
new_compare0(Neg(Zero), Pos(Succ(x0)))
new_compare7(x0, x1, x2, x3)
new_primCmpNat0(x0, Succ(x1))
new_primCmpNat0(x0, Zero)
new_compare0(Pos(Zero), Neg(Zero))
new_compare0(Neg(Zero), Pos(Zero))
new_compare(x0, x1, ty_Int)
new_compare0(Pos(Succ(x0)), Pos(x1))
new_compare(x0, x1, app(ty_Maybe, x2))
new_compare2(x0, x1, x2)
new_compare9(x0, x1)
new_compare0(Neg(Zero), Neg(Zero))
new_primCmpNat1(Succ(x0), x1)
new_compare1(x0, x1)
new_compare(x0, x1, app(app(ty_Either, x2), x3))
new_compare(x0, x1, ty_Double)
new_compare12(x0, x1, x2)
new_compare10(x0, x1)
new_compare0(Pos(Succ(x0)), Neg(x1))
new_compare0(Neg(Succ(x0)), Pos(x1))
new_primCmpNat2(Succ(x0), Zero)
new_compare11(x0, x1)
new_compare(x0, x1, app(ty_Ratio, x2))
new_compare(x0, x1, ty_Bool)
new_compare(x0, x1, app(ty_[], x2))
new_compare4(x0, x1)
new_primCmpNat1(Zero, x0)
new_compare(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare13(x0, x1)
new_compare6(x0, x1, x2, x3)
new_compare(x0, x1, ty_Float)
new_primCmpNat2(Zero, Zero)
new_compare(x0, x1, ty_Integer)
new_primCmpNat2(Succ(x0), Succ(x1))
new_compare0(Pos(Zero), Pos(Succ(x0)))
new_compare(x0, x1, ty_Ordering)
new_compare0(Pos(Zero), Pos(Zero))
new_compare(x0, x1, app(app(ty_@2, x2), x3))
new_compare0(Neg(Zero), Neg(Succ(x0)))
new_primCmpNat2(Zero, Succ(x0))
new_compare(x0, x1, ty_Char)
new_compare3(x0, x1, x2, x3, x4)
new_compare5(x0, x1)
new_compare(x0, x1, ty_@0)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

new_merge0(vz127, vz128, vz129, vz130, EQ, ba) → new_merge(vz129, :(vz127, vz130), ba)
new_merge0(vz127, vz128, vz129, vz130, LT, ba) → new_merge(vz129, :(vz127, vz130), ba)

The remaining pairs can at least be oriented weakly.

new_merge0(vz127, vz128, vz129, vz130, GT, ba) → new_merge(:(vz128, vz129), vz130, ba)
new_merge(:(vz1170, vz1171), :(vz11800, vz11801), bb) → new_merge0(vz11800, vz1170, vz1171, vz11801, new_compare(vz1170, vz11800, bb), bb)

Used ordering: Polynomial interpretation [25]:

POL(:(x₁, x₂)) = 1 + x₂
POL(EQ) = 0
POL(GT) = 0
POL(LT) = 0
POL(Neg(x₁)) = 0
POL(Pos(x₁)) = 0
POL(Succ(x₁)) = 0
POL(Zero) = 0
POL([]) = 0
POL(app(x₁, x₂)) = 0
POL(error(x₁)) = 0
POL(new_compare(x₁, x₂, x₃)) = 0
POL(new_compare0(x₁, x₂)) = 0
POL(new_compare1(x₁, x₂)) = 0
POL(new_compare10(x₁, x₂)) = 0
POL(new_compare11(x₁, x₂)) = 0
POL(new_compare12(x₁, x₂, x₃)) = 0
POL(new_compare13(x₁, x₂)) = 0
POL(new_compare2(x₁, x₂, x₃)) = 0
POL(new_compare3(x₁, x₂, x₃, x₄, x₅)) = 0
POL(new_compare4(x₁, x₂)) = 0
POL(new_compare5(x₁, x₂)) = 0
POL(new_compare6(x₁, x₂, x₃, x₄)) = 0
POL(new_compare7(x₁, x₂, x₃, x₄)) = 0
POL(new_compare8(x₁, x₂, x₃)) = 0
POL(new_compare9(x₁, x₂)) = 0
POL(new_merge(x₁, x₂, x₃)) = x₁
POL(new_merge0(x₁, x₂, x₃, x₄, x₅, x₆)) = 1 + x₃
POL(new_primCmpNat0(x₁, x₂)) = 0
POL(new_primCmpNat1(x₁, x₂)) = 0
POL(new_primCmpNat2(x₁, x₂)) = 0
POL(ty_@0) = 0
POL(ty_@2) = 0
POL(ty_@3) = 0
POL(ty_Bool) = 0
POL(ty_Char) = 0
POL(ty_Double) = 0
POL(ty_Either) = 0
POL(ty_Float) = 0
POL(ty_Int) = 0
POL(ty_Integer) = 0
POL(ty_Maybe) = 0
POL(ty_Ordering) = 0
POL(ty_Ratio) = 0
POL(ty_[]) = 0

The following usable rules [17] were oriented: none

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_merge0(vz127, vz128, vz129, vz130, GT, ba) → new_merge(:(vz128, vz129), vz130, ba)
new_merge(:(vz1170, vz1171), :(vz11800, vz11801), bb) → new_merge0(vz11800, vz1170, vz1171, vz11801, new_compare(vz1170, vz11800, bb), bb)

The TRS R consists of the following rules:

new_compare2(vz1170, vz11800, bc) → error([])
new_compare(vz1170, vz11800, ty_Int) → new_compare0(vz1170, vz11800)
new_compare3(vz1170, vz11800, bd, be, bf) → error([])
new_compare(vz1170, vz11800, app(ty_Ratio, bc)) → new_compare2(vz1170, vz11800, bc)
new_compare(vz1170, vz11800, app(ty_Maybe, cd)) → new_compare12(vz1170, vz11800, cd)
new_primCmpNat0(vz120000, Succ(vz119000)) → new_primCmpNat2(vz120000, vz119000)
new_compare(vz1170, vz11800, app(ty_[], cc)) → new_compare8(vz1170, vz11800, cc)
new_compare4(vz1170, vz11800) → error([])
new_compare7(vz1170, vz11800, ca, cb) → error([])
new_compare0(Neg(Zero), Pos(Succ(vz119000))) → LT
new_compare(vz1170, vz11800, ty_Bool) → new_compare11(vz1170, vz11800)
new_compare10(vz1170, vz11800) → error([])
new_compare(vz1170, vz11800, ty_Integer) → new_compare13(vz1170, vz11800)
new_compare(vz1170, vz11800, ty_Float) → new_compare4(vz1170, vz11800)
new_compare(vz1170, vz11800, ty_Char) → new_compare1(vz1170, vz11800)
new_compare0(Neg(Succ(vz120000)), Pos(vz11900)) → LT
new_compare0(Neg(Zero), Neg(Zero)) → EQ
new_compare(vz1170, vz11800, ty_@0) → new_compare5(vz1170, vz11800)
new_compare1(vz1170, vz11800) → error([])
new_primCmpNat2(Zero, Zero) → EQ
new_compare0(Pos(Succ(vz120000)), Pos(vz11900)) → new_primCmpNat0(vz120000, vz11900)
new_compare(vz1170, vz11800, ty_Double) → new_compare9(vz1170, vz11800)
new_compare(vz1170, vz11800, app(app(ty_Either, bg), bh)) → new_compare6(vz1170, vz11800, bg, bh)
new_compare8(vz1170, vz11800, cc) → error([])
new_primCmpNat2(Zero, Succ(vz1190000)) → LT
new_compare5(vz1170, vz11800) → error([])
new_compare11(vz1170, vz11800) → error([])
new_compare(vz1170, vz11800, app(app(app(ty_@3, bd), be), bf)) → new_compare3(vz1170, vz11800, bd, be, bf)
new_compare0(Pos(Zero), Pos(Succ(vz119000))) → new_primCmpNat1(Zero, vz119000)
new_compare(vz1170, vz11800, app(app(ty_@2, ca), cb)) → new_compare7(vz1170, vz11800, ca, cb)
new_compare12(vz1170, vz11800, cd) → error([])
new_compare9(vz1170, vz11800) → error([])
new_primCmpNat1(Succ(vz119000), vz120000) → new_primCmpNat2(vz119000, vz120000)
new_compare(vz1170, vz11800, ty_Ordering) → new_compare10(vz1170, vz11800)
new_primCmpNat2(Succ(vz1200000), Succ(vz1190000)) → new_primCmpNat2(vz1200000, vz1190000)
new_primCmpNat2(Succ(vz1200000), Zero) → GT
new_compare0(Pos(Zero), Neg(Zero)) → EQ
new_compare0(Neg(Zero), Pos(Zero)) → EQ
new_compare0(Neg(Zero), Neg(Succ(vz119000))) → new_primCmpNat0(vz119000, Zero)
new_compare0(Pos(Succ(vz120000)), Neg(vz11900)) → GT
new_compare0(Neg(Succ(vz120000)), Neg(vz11900)) → new_primCmpNat1(vz11900, vz120000)
new_primCmpNat1(Zero, vz120000) → LT
new_compare13(vz1170, vz11800) → error([])
new_compare0(Pos(Zero), Pos(Zero)) → EQ
new_compare6(vz1170, vz11800, bg, bh) → error([])
new_primCmpNat0(vz120000, Zero) → GT
new_compare0(Pos(Zero), Neg(Succ(vz119000))) → GT

The set Q consists of the following terms:

new_compare8(x0, x1, x2)
new_compare0(Neg(Succ(x0)), Neg(x1))
new_compare0(Pos(Zero), Neg(Succ(x0)))
new_compare0(Neg(Zero), Pos(Succ(x0)))
new_compare7(x0, x1, x2, x3)
new_primCmpNat0(x0, Succ(x1))
new_primCmpNat0(x0, Zero)
new_compare0(Pos(Zero), Neg(Zero))
new_compare0(Neg(Zero), Pos(Zero))
new_compare(x0, x1, ty_Int)
new_compare0(Pos(Succ(x0)), Pos(x1))
new_compare(x0, x1, app(ty_Maybe, x2))
new_compare2(x0, x1, x2)
new_compare9(x0, x1)
new_compare0(Neg(Zero), Neg(Zero))
new_primCmpNat1(Succ(x0), x1)
new_compare1(x0, x1)
new_compare(x0, x1, app(app(ty_Either, x2), x3))
new_compare(x0, x1, ty_Double)
new_compare12(x0, x1, x2)
new_compare10(x0, x1)
new_compare0(Pos(Succ(x0)), Neg(x1))
new_compare0(Neg(Succ(x0)), Pos(x1))
new_primCmpNat2(Succ(x0), Zero)
new_compare11(x0, x1)
new_compare(x0, x1, app(ty_Ratio, x2))
new_compare(x0, x1, ty_Bool)
new_compare(x0, x1, app(ty_[], x2))
new_compare4(x0, x1)
new_primCmpNat1(Zero, x0)
new_compare(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare13(x0, x1)
new_compare6(x0, x1, x2, x3)
new_compare(x0, x1, ty_Float)
new_primCmpNat2(Zero, Zero)
new_compare(x0, x1, ty_Integer)
new_primCmpNat2(Succ(x0), Succ(x1))
new_compare0(Pos(Zero), Pos(Succ(x0)))
new_compare(x0, x1, ty_Ordering)
new_compare0(Pos(Zero), Pos(Zero))
new_compare(x0, x1, app(app(ty_@2, x2), x3))
new_compare0(Neg(Zero), Neg(Succ(x0)))
new_primCmpNat2(Zero, Succ(x0))
new_compare(x0, x1, ty_Char)
new_compare3(x0, x1, x2, x3, x4)
new_compare5(x0, x1)
new_compare(x0, x1, ty_@0)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_merge(:(vz1170, vz1171), :(vz11800, vz11801), bb) → new_merge0(vz11800, vz1170, vz1171, vz11801, new_compare(vz1170, vz11800, bb), bb)
The graph contains the following edges 2 > 1, 1 > 2, 1 > 3, 2 > 4, 3 >= 6
new_merge0(vz127, vz128, vz129, vz130, GT, ba) → new_merge(:(vz128, vz129), vz130, ba)
The graph contains the following edges 4 >= 2, 6 >= 3

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_merge_pairs(:(vz118110, :(vz1181110, vz1181111)), ba) → new_merge_pairs(vz1181111, ba)

From the DPs we obtained the following set of size-change graphs:

new_merge_pairs(:(vz118110, :(vz1181110, vz1181111)), ba) → new_merge_pairs(vz1181111, ba)
The graph contains the following edges 1 > 1, 2 >= 2

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

new_mergesort'(vz117, :(vz1180, []), ba) → new_mergesort'(new_merge2(vz117, vz1180, ba), [], ba)
new_mergesort'(vz117, :(vz1180, :(vz11810, vz11811)), ba) → new_mergesort'(new_merge1(vz117, vz1180, vz11810, ba), new_merge_pairs0(vz11811, ba), ba)

The TRS R consists of the following rules:

new_compare2(vz1170, vz11800, bb) → error([])
new_compare14(vz11800, vz118100, ty_Int) → new_compare0(vz11800, vz118100)
new_primCmpNat0(vz120000, Succ(vz119000)) → new_primCmpNat2(vz120000, vz119000)
new_compare(vz1170, vz11800, app(ty_Ratio, bb)) → new_compare2(vz1170, vz11800, bb)
new_compare(vz1170, vz11800, app(ty_Maybe, cd)) → new_compare12(vz1170, vz11800, cd)
new_compare7(vz1170, vz11800, ca, cb) → error([])
new_compare14(vz11800, vz118100, app(ty_Maybe, cd)) → new_compare12(vz11800, vz118100, cd)
new_compare10(vz1170, vz11800) → error([])
new_compare(vz1170, vz11800, ty_Integer) → new_compare13(vz1170, vz11800)
new_merge00(vz127, vz128, vz129, vz130, LT, bf) → :(vz128, new_merge2(vz129, :(vz127, vz130), bf))
new_compare(vz1170, vz11800, ty_Float) → new_compare4(vz1170, vz11800)
new_compare14(vz11800, vz118100, ty_Bool) → new_compare11(vz11800, vz118100)
new_compare(vz1170, vz11800, ty_Char) → new_compare1(vz1170, vz11800)
new_merge_pairs0(:(vz118110, :(vz1181110, vz1181111)), ba) → :(new_merge2(vz118110, vz1181110, ba), new_merge_pairs0(vz1181111, ba))
new_compare14(vz11800, vz118100, ty_Char) → new_compare1(vz11800, vz118100)
new_compare14(vz11800, vz118100, app(app(ty_@2, ca), cb)) → new_compare7(vz11800, vz118100, ca, cb)
new_merge1(vz117, [], :(vz118100, vz118101), ba) → new_merge2(vz117, :(vz118100, vz118101), ba)
new_merge_pairs0(:(vz118110, []), ba) → :(vz118110, [])
new_compare0(Neg(Zero), Neg(Zero)) → EQ
new_compare0(Neg(Succ(vz120000)), Pos(vz11900)) → LT
new_primCmpNat2(Zero, Zero) → EQ
new_merge1(vz117, :(vz11800, vz11801), :(vz118100, vz118101), ba) → new_merge2(vz117, new_merge00(vz118100, vz11800, vz11801, vz118101, new_compare14(vz11800, vz118100, ba), ba), ba)
new_compare(vz1170, vz11800, ty_Double) → new_compare9(vz1170, vz11800)
new_compare14(vz11800, vz118100, ty_Ordering) → new_compare10(vz11800, vz118100)
new_compare(vz1170, vz11800, app(app(ty_Either, bg), bh)) → new_compare6(vz1170, vz11800, bg, bh)
new_compare14(vz11800, vz118100, ty_Double) → new_compare9(vz11800, vz118100)
new_primCmpNat2(Zero, Succ(vz1190000)) → LT
new_compare14(vz11800, vz118100, app(ty_[], cc)) → new_compare8(vz11800, vz118100, cc)
new_merge00(vz127, vz128, vz129, vz130, GT, bf) → :(vz127, new_merge2(:(vz128, vz129), vz130, bf))
new_compare12(vz1170, vz11800, cd) → error([])
new_compare9(vz1170, vz11800) → error([])
new_primCmpNat1(Succ(vz119000), vz120000) → new_primCmpNat2(vz119000, vz120000)
new_compare14(vz11800, vz118100, ty_Integer) → new_compare13(vz11800, vz118100)
new_compare14(vz11800, vz118100, ty_Float) → new_compare4(vz11800, vz118100)
new_primCmpNat2(Succ(vz1200000), Zero) → GT
new_primCmpNat2(Succ(vz1200000), Succ(vz1190000)) → new_primCmpNat2(vz1200000, vz1190000)
new_compare0(Neg(Zero), Neg(Succ(vz119000))) → new_primCmpNat0(vz119000, Zero)
new_compare0(Pos(Succ(vz120000)), Neg(vz11900)) → GT
new_compare0(Neg(Succ(vz120000)), Neg(vz11900)) → new_primCmpNat1(vz11900, vz120000)
new_compare6(vz1170, vz11800, bg, bh) → error([])
new_primCmpNat0(vz120000, Zero) → GT
new_merge2([], :(vz11800, vz11801), ba) → :(vz11800, vz11801)
new_compare0(Pos(Zero), Neg(Succ(vz119000))) → GT
new_compare(vz1170, vz11800, ty_Int) → new_compare0(vz1170, vz11800)
new_merge_pairs0([], ba) → []
new_compare3(vz1170, vz11800, bc, bd, be) → error([])
new_compare4(vz1170, vz11800) → error([])
new_compare(vz1170, vz11800, app(ty_[], cc)) → new_compare8(vz1170, vz11800, cc)
new_compare0(Neg(Zero), Pos(Succ(vz119000))) → LT
new_compare(vz1170, vz11800, ty_Bool) → new_compare11(vz1170, vz11800)
new_merge1(vz117, vz1180, [], ba) → new_merge2(vz117, vz1180, ba)
new_merge2(:(vz1170, vz1171), :(vz11800, vz11801), ba) → new_merge00(vz11800, vz1170, vz1171, vz11801, new_compare(vz1170, vz11800, ba), ba)
new_compare(vz1170, vz11800, ty_@0) → new_compare5(vz1170, vz11800)
new_merge2(vz117, [], ba) → vz117
new_compare1(vz1170, vz11800) → error([])
new_compare0(Pos(Succ(vz120000)), Pos(vz11900)) → new_primCmpNat0(vz120000, vz11900)
new_compare8(vz1170, vz11800, cc) → error([])
new_compare14(vz11800, vz118100, app(app(ty_Either, bg), bh)) → new_compare6(vz11800, vz118100, bg, bh)
new_compare5(vz1170, vz11800) → error([])
new_compare11(vz1170, vz11800) → error([])
new_compare0(Pos(Zero), Pos(Succ(vz119000))) → new_primCmpNat1(Zero, vz119000)
new_compare(vz1170, vz11800, app(app(app(ty_@3, bc), bd), be)) → new_compare3(vz1170, vz11800, bc, bd, be)
new_compare(vz1170, vz11800, app(app(ty_@2, ca), cb)) → new_compare7(vz1170, vz11800, ca, cb)
new_compare(vz1170, vz11800, ty_Ordering) → new_compare10(vz1170, vz11800)
new_compare14(vz11800, vz118100, app(ty_Ratio, bb)) → new_compare2(vz11800, vz118100, bb)
new_compare0(Neg(Zero), Pos(Zero)) → EQ
new_compare0(Pos(Zero), Neg(Zero)) → EQ
new_merge00(vz127, vz128, vz129, vz130, EQ, bf) → :(vz128, new_merge2(vz129, :(vz127, vz130), bf))
new_primCmpNat1(Zero, vz120000) → LT
new_compare13(vz1170, vz11800) → error([])
new_compare0(Pos(Zero), Pos(Zero)) → EQ
new_compare14(vz11800, vz118100, ty_@0) → new_compare5(vz11800, vz118100)
new_compare14(vz11800, vz118100, app(app(app(ty_@3, bc), bd), be)) → new_compare3(vz11800, vz118100, bc, bd, be)

The set Q consists of the following terms:

new_compare8(x0, x1, x2)
new_compare0(Neg(Succ(x0)), Neg(x1))
new_merge1(x0, x1, [], x2)
new_compare0(Neg(Zero), Pos(Succ(x0)))
new_compare0(Pos(Zero), Neg(Succ(x0)))
new_primCmpNat0(x0, Succ(x1))
new_compare14(x0, x1, ty_Ordering)
new_compare0(Neg(Zero), Pos(Zero))
new_compare0(Pos(Zero), Neg(Zero))
new_primCmpNat0(x0, Zero)
new_compare(x0, x1, app(ty_Ratio, x2))
new_compare14(x0, x1, ty_Bool)
new_compare14(x0, x1, ty_Integer)
new_compare(x0, x1, ty_Int)
new_compare0(Pos(Succ(x0)), Pos(x1))
new_compare0(Neg(Zero), Neg(Zero))
new_merge_pairs0(:(x0, []), x1)
new_compare10(x0, x1)
new_compare12(x0, x1, x2)
new_compare0(Neg(Succ(x0)), Pos(x1))
new_compare0(Pos(Succ(x0)), Neg(x1))
new_compare11(x0, x1)
new_primCmpNat2(Succ(x0), Zero)
new_compare4(x0, x1)
new_compare14(x0, x1, app(ty_[], x2))
new_compare13(x0, x1)
new_compare14(x0, x1, app(ty_Maybe, x2))
new_primCmpNat2(Zero, Zero)
new_compare(x0, x1, ty_Integer)
new_primCmpNat2(Succ(x0), Succ(x1))
new_compare14(x0, x1, ty_@0)
new_compare(x0, x1, ty_Ordering)
new_compare(x0, x1, app(app(ty_@2, x2), x3))
new_compare2(x0, x1, x2)
new_merge00(x0, x1, x2, x3, EQ, x4)
new_compare(x0, x1, ty_Char)
new_compare5(x0, x1)
new_compare(x0, x1, ty_@0)
new_merge2(:(x0, x1), :(x2, x3), x4)
new_merge00(x0, x1, x2, x3, LT, x4)
new_compare14(x0, x1, ty_Int)
new_compare7(x0, x1, x2, x3)
new_merge1(x0, :(x1, x2), :(x3, x4), x5)
new_merge1(x0, [], :(x1, x2), x3)
new_merge_pairs0([], x0)
new_merge_pairs0(:(x0, :(x1, x2)), x3)
new_compare(x0, x1, app(ty_Maybe, x2))
new_compare14(x0, x1, ty_Char)
new_compare9(x0, x1)
new_compare1(x0, x1)
new_compare(x0, x1, app(app(ty_Either, x2), x3))
new_primCmpNat1(Succ(x0), x1)
new_compare14(x0, x1, app(app(ty_@2, x2), x3))
new_compare(x0, x1, ty_Double)
new_merge2(x0, [], x1)
new_compare14(x0, x1, app(app(ty_Either, x2), x3))
new_merge2([], :(x0, x1), x2)
new_compare14(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare(x0, x1, app(ty_[], x2))
new_compare(x0, x1, ty_Bool)
new_primCmpNat1(Zero, x0)
new_compare(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare3(x0, x1, x2, x3, x4)
new_compare14(x0, x1, ty_Double)
new_compare14(x0, x1, app(ty_Ratio, x2))
new_compare6(x0, x1, x2, x3)
new_compare(x0, x1, ty_Float)
new_merge00(x0, x1, x2, x3, GT, x4)
new_compare0(Pos(Zero), Pos(Succ(x0)))
new_compare0(Pos(Zero), Pos(Zero))
new_compare14(x0, x1, ty_Float)
new_compare0(Neg(Zero), Neg(Succ(x0)))
new_primCmpNat2(Zero, Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ QDP

                        ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

new_mergesort'(vz117, :(vz1180, :(vz11810, vz11811)), ba) → new_mergesort'(new_merge1(vz117, vz1180, vz11810, ba), new_merge_pairs0(vz11811, ba), ba)

The TRS R consists of the following rules:

new_compare2(vz1170, vz11800, bb) → error([])
new_compare14(vz11800, vz118100, ty_Int) → new_compare0(vz11800, vz118100)
new_primCmpNat0(vz120000, Succ(vz119000)) → new_primCmpNat2(vz120000, vz119000)
new_compare(vz1170, vz11800, app(ty_Ratio, bb)) → new_compare2(vz1170, vz11800, bb)
new_compare(vz1170, vz11800, app(ty_Maybe, cd)) → new_compare12(vz1170, vz11800, cd)
new_compare7(vz1170, vz11800, ca, cb) → error([])
new_compare14(vz11800, vz118100, app(ty_Maybe, cd)) → new_compare12(vz11800, vz118100, cd)
new_compare10(vz1170, vz11800) → error([])
new_compare(vz1170, vz11800, ty_Integer) → new_compare13(vz1170, vz11800)
new_merge00(vz127, vz128, vz129, vz130, LT, bf) → :(vz128, new_merge2(vz129, :(vz127, vz130), bf))
new_compare(vz1170, vz11800, ty_Float) → new_compare4(vz1170, vz11800)
new_compare14(vz11800, vz118100, ty_Bool) → new_compare11(vz11800, vz118100)
new_compare(vz1170, vz11800, ty_Char) → new_compare1(vz1170, vz11800)
new_merge_pairs0(:(vz118110, :(vz1181110, vz1181111)), ba) → :(new_merge2(vz118110, vz1181110, ba), new_merge_pairs0(vz1181111, ba))
new_compare14(vz11800, vz118100, ty_Char) → new_compare1(vz11800, vz118100)
new_compare14(vz11800, vz118100, app(app(ty_@2, ca), cb)) → new_compare7(vz11800, vz118100, ca, cb)
new_merge1(vz117, [], :(vz118100, vz118101), ba) → new_merge2(vz117, :(vz118100, vz118101), ba)
new_merge_pairs0(:(vz118110, []), ba) → :(vz118110, [])
new_compare0(Neg(Zero), Neg(Zero)) → EQ
new_compare0(Neg(Succ(vz120000)), Pos(vz11900)) → LT
new_primCmpNat2(Zero, Zero) → EQ
new_merge1(vz117, :(vz11800, vz11801), :(vz118100, vz118101), ba) → new_merge2(vz117, new_merge00(vz118100, vz11800, vz11801, vz118101, new_compare14(vz11800, vz118100, ba), ba), ba)
new_compare(vz1170, vz11800, ty_Double) → new_compare9(vz1170, vz11800)
new_compare14(vz11800, vz118100, ty_Ordering) → new_compare10(vz11800, vz118100)
new_compare(vz1170, vz11800, app(app(ty_Either, bg), bh)) → new_compare6(vz1170, vz11800, bg, bh)
new_compare14(vz11800, vz118100, ty_Double) → new_compare9(vz11800, vz118100)
new_primCmpNat2(Zero, Succ(vz1190000)) → LT
new_compare14(vz11800, vz118100, app(ty_[], cc)) → new_compare8(vz11800, vz118100, cc)
new_merge00(vz127, vz128, vz129, vz130, GT, bf) → :(vz127, new_merge2(:(vz128, vz129), vz130, bf))
new_compare12(vz1170, vz11800, cd) → error([])
new_compare9(vz1170, vz11800) → error([])
new_primCmpNat1(Succ(vz119000), vz120000) → new_primCmpNat2(vz119000, vz120000)
new_compare14(vz11800, vz118100, ty_Integer) → new_compare13(vz11800, vz118100)
new_compare14(vz11800, vz118100, ty_Float) → new_compare4(vz11800, vz118100)
new_primCmpNat2(Succ(vz1200000), Zero) → GT
new_primCmpNat2(Succ(vz1200000), Succ(vz1190000)) → new_primCmpNat2(vz1200000, vz1190000)
new_compare0(Neg(Zero), Neg(Succ(vz119000))) → new_primCmpNat0(vz119000, Zero)
new_compare0(Pos(Succ(vz120000)), Neg(vz11900)) → GT
new_compare0(Neg(Succ(vz120000)), Neg(vz11900)) → new_primCmpNat1(vz11900, vz120000)
new_compare6(vz1170, vz11800, bg, bh) → error([])
new_primCmpNat0(vz120000, Zero) → GT
new_merge2([], :(vz11800, vz11801), ba) → :(vz11800, vz11801)
new_compare0(Pos(Zero), Neg(Succ(vz119000))) → GT
new_compare(vz1170, vz11800, ty_Int) → new_compare0(vz1170, vz11800)
new_merge_pairs0([], ba) → []
new_compare3(vz1170, vz11800, bc, bd, be) → error([])
new_compare4(vz1170, vz11800) → error([])
new_compare(vz1170, vz11800, app(ty_[], cc)) → new_compare8(vz1170, vz11800, cc)
new_compare0(Neg(Zero), Pos(Succ(vz119000))) → LT
new_compare(vz1170, vz11800, ty_Bool) → new_compare11(vz1170, vz11800)
new_merge1(vz117, vz1180, [], ba) → new_merge2(vz117, vz1180, ba)
new_merge2(:(vz1170, vz1171), :(vz11800, vz11801), ba) → new_merge00(vz11800, vz1170, vz1171, vz11801, new_compare(vz1170, vz11800, ba), ba)
new_compare(vz1170, vz11800, ty_@0) → new_compare5(vz1170, vz11800)
new_merge2(vz117, [], ba) → vz117
new_compare1(vz1170, vz11800) → error([])
new_compare0(Pos(Succ(vz120000)), Pos(vz11900)) → new_primCmpNat0(vz120000, vz11900)
new_compare8(vz1170, vz11800, cc) → error([])
new_compare14(vz11800, vz118100, app(app(ty_Either, bg), bh)) → new_compare6(vz11800, vz118100, bg, bh)
new_compare5(vz1170, vz11800) → error([])
new_compare11(vz1170, vz11800) → error([])
new_compare0(Pos(Zero), Pos(Succ(vz119000))) → new_primCmpNat1(Zero, vz119000)
new_compare(vz1170, vz11800, app(app(app(ty_@3, bc), bd), be)) → new_compare3(vz1170, vz11800, bc, bd, be)
new_compare(vz1170, vz11800, app(app(ty_@2, ca), cb)) → new_compare7(vz1170, vz11800, ca, cb)
new_compare(vz1170, vz11800, ty_Ordering) → new_compare10(vz1170, vz11800)
new_compare14(vz11800, vz118100, app(ty_Ratio, bb)) → new_compare2(vz11800, vz118100, bb)
new_compare0(Neg(Zero), Pos(Zero)) → EQ
new_compare0(Pos(Zero), Neg(Zero)) → EQ
new_merge00(vz127, vz128, vz129, vz130, EQ, bf) → :(vz128, new_merge2(vz129, :(vz127, vz130), bf))
new_primCmpNat1(Zero, vz120000) → LT
new_compare13(vz1170, vz11800) → error([])
new_compare0(Pos(Zero), Pos(Zero)) → EQ
new_compare14(vz11800, vz118100, ty_@0) → new_compare5(vz11800, vz118100)
new_compare14(vz11800, vz118100, app(app(app(ty_@3, bc), bd), be)) → new_compare3(vz11800, vz118100, bc, bd, be)

The set Q consists of the following terms:

new_compare8(x0, x1, x2)
new_compare0(Neg(Succ(x0)), Neg(x1))
new_merge1(x0, x1, [], x2)
new_compare0(Neg(Zero), Pos(Succ(x0)))
new_compare0(Pos(Zero), Neg(Succ(x0)))
new_primCmpNat0(x0, Succ(x1))
new_compare14(x0, x1, ty_Ordering)
new_compare0(Neg(Zero), Pos(Zero))
new_compare0(Pos(Zero), Neg(Zero))
new_primCmpNat0(x0, Zero)
new_compare(x0, x1, app(ty_Ratio, x2))
new_compare14(x0, x1, ty_Bool)
new_compare14(x0, x1, ty_Integer)
new_compare(x0, x1, ty_Int)
new_compare0(Pos(Succ(x0)), Pos(x1))
new_compare0(Neg(Zero), Neg(Zero))
new_merge_pairs0(:(x0, []), x1)
new_compare10(x0, x1)
new_compare12(x0, x1, x2)
new_compare0(Neg(Succ(x0)), Pos(x1))
new_compare0(Pos(Succ(x0)), Neg(x1))
new_compare11(x0, x1)
new_primCmpNat2(Succ(x0), Zero)
new_compare4(x0, x1)
new_compare14(x0, x1, app(ty_[], x2))
new_compare13(x0, x1)
new_compare14(x0, x1, app(ty_Maybe, x2))
new_primCmpNat2(Zero, Zero)
new_compare(x0, x1, ty_Integer)
new_primCmpNat2(Succ(x0), Succ(x1))
new_compare14(x0, x1, ty_@0)
new_compare(x0, x1, ty_Ordering)
new_compare(x0, x1, app(app(ty_@2, x2), x3))
new_compare2(x0, x1, x2)
new_merge00(x0, x1, x2, x3, EQ, x4)
new_compare(x0, x1, ty_Char)
new_compare5(x0, x1)
new_compare(x0, x1, ty_@0)
new_merge2(:(x0, x1), :(x2, x3), x4)
new_merge00(x0, x1, x2, x3, LT, x4)
new_compare14(x0, x1, ty_Int)
new_compare7(x0, x1, x2, x3)
new_merge1(x0, :(x1, x2), :(x3, x4), x5)
new_merge1(x0, [], :(x1, x2), x3)
new_merge_pairs0([], x0)
new_merge_pairs0(:(x0, :(x1, x2)), x3)
new_compare(x0, x1, app(ty_Maybe, x2))
new_compare14(x0, x1, ty_Char)
new_compare9(x0, x1)
new_compare1(x0, x1)
new_compare(x0, x1, app(app(ty_Either, x2), x3))
new_primCmpNat1(Succ(x0), x1)
new_compare14(x0, x1, app(app(ty_@2, x2), x3))
new_compare(x0, x1, ty_Double)
new_merge2(x0, [], x1)
new_compare14(x0, x1, app(app(ty_Either, x2), x3))
new_merge2([], :(x0, x1), x2)
new_compare14(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare(x0, x1, app(ty_[], x2))
new_compare(x0, x1, ty_Bool)
new_primCmpNat1(Zero, x0)
new_compare(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare3(x0, x1, x2, x3, x4)
new_compare14(x0, x1, ty_Double)
new_compare14(x0, x1, app(ty_Ratio, x2))
new_compare6(x0, x1, x2, x3)
new_compare(x0, x1, ty_Float)
new_merge00(x0, x1, x2, x3, GT, x4)
new_compare0(Pos(Zero), Pos(Succ(x0)))
new_compare0(Pos(Zero), Pos(Zero))
new_compare14(x0, x1, ty_Float)
new_compare0(Neg(Zero), Neg(Succ(x0)))
new_primCmpNat2(Zero, Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

new_mergesort'(vz117, :(vz1180, :(vz11810, vz11811)), ba) → new_mergesort'(new_merge1(vz117, vz1180, vz11810, ba), new_merge_pairs0(vz11811, ba), ba)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25]:

POL(:(x₁, x₂)) = 1 + x₂
POL(EQ) = 1
POL(GT) = 1
POL(LT) = 1
POL(Neg(x₁)) = 0
POL(Pos(x₁)) = 0
POL(Succ(x₁)) = 0
POL(Zero) = 0
POL([]) = 1
POL(app(x₁, x₂)) = 0
POL(error(x₁)) = 0
POL(new_compare(x₁, x₂, x₃)) = 0
POL(new_compare0(x₁, x₂)) = 0
POL(new_compare1(x₁, x₂)) = 0
POL(new_compare10(x₁, x₂)) = 0
POL(new_compare11(x₁, x₂)) = 0
POL(new_compare12(x₁, x₂, x₃)) = 0
POL(new_compare13(x₁, x₂)) = 0
POL(new_compare14(x₁, x₂, x₃)) = 0
POL(new_compare2(x₁, x₂, x₃)) = 0
POL(new_compare3(x₁, x₂, x₃, x₄, x₅)) = 0
POL(new_compare4(x₁, x₂)) = 0
POL(new_compare5(x₁, x₂)) = 0
POL(new_compare6(x₁, x₂, x₃, x₄)) = 0
POL(new_compare7(x₁, x₂, x₃, x₄)) = 0
POL(new_compare8(x₁, x₂, x₃)) = 0
POL(new_compare9(x₁, x₂)) = 0
POL(new_merge00(x₁, x₂, x₃, x₄, x₅, x₆)) = 1 + x₃ + x₄ + x₅
POL(new_merge1(x₁, x₂, x₃, x₄)) = 0
POL(new_merge2(x₁, x₂, x₃)) = x₁ + x₂
POL(new_merge_pairs0(x₁, x₂)) = 1 + x₁
POL(new_mergesort'(x₁, x₂, x₃)) = x₂
POL(new_primCmpNat0(x₁, x₂)) = 0
POL(new_primCmpNat1(x₁, x₂)) = 0
POL(new_primCmpNat2(x₁, x₂)) = 0
POL(ty_@0) = 0
POL(ty_@2) = 0
POL(ty_@3) = 0
POL(ty_Bool) = 0
POL(ty_Char) = 0
POL(ty_Double) = 0
POL(ty_Either) = 0
POL(ty_Float) = 0
POL(ty_Int) = 0
POL(ty_Integer) = 0
POL(ty_Maybe) = 0
POL(ty_Ordering) = 0
POL(ty_Ratio) = 0
POL(ty_[]) = 0

The following usable rules [17] were oriented:

new_merge_pairs0(:(vz118110, []), ba) → :(vz118110, [])
new_merge_pairs0(:(vz118110, :(vz1181110, vz1181111)), ba) → :(new_merge2(vz118110, vz1181110, ba), new_merge_pairs0(vz1181111, ba))
new_merge_pairs0([], ba) → []

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ PisEmptyProof

Q DP problem:
P is empty.
The TRS R consists of the following rules:

new_compare2(vz1170, vz11800, bb) → error([])
new_compare14(vz11800, vz118100, ty_Int) → new_compare0(vz11800, vz118100)
new_primCmpNat0(vz120000, Succ(vz119000)) → new_primCmpNat2(vz120000, vz119000)
new_compare(vz1170, vz11800, app(ty_Ratio, bb)) → new_compare2(vz1170, vz11800, bb)
new_compare(vz1170, vz11800, app(ty_Maybe, cd)) → new_compare12(vz1170, vz11800, cd)
new_compare7(vz1170, vz11800, ca, cb) → error([])
new_compare14(vz11800, vz118100, app(ty_Maybe, cd)) → new_compare12(vz11800, vz118100, cd)
new_compare10(vz1170, vz11800) → error([])
new_compare(vz1170, vz11800, ty_Integer) → new_compare13(vz1170, vz11800)
new_merge00(vz127, vz128, vz129, vz130, LT, bf) → :(vz128, new_merge2(vz129, :(vz127, vz130), bf))
new_compare(vz1170, vz11800, ty_Float) → new_compare4(vz1170, vz11800)
new_compare14(vz11800, vz118100, ty_Bool) → new_compare11(vz11800, vz118100)
new_compare(vz1170, vz11800, ty_Char) → new_compare1(vz1170, vz11800)
new_merge_pairs0(:(vz118110, :(vz1181110, vz1181111)), ba) → :(new_merge2(vz118110, vz1181110, ba), new_merge_pairs0(vz1181111, ba))
new_compare14(vz11800, vz118100, ty_Char) → new_compare1(vz11800, vz118100)
new_compare14(vz11800, vz118100, app(app(ty_@2, ca), cb)) → new_compare7(vz11800, vz118100, ca, cb)
new_merge1(vz117, [], :(vz118100, vz118101), ba) → new_merge2(vz117, :(vz118100, vz118101), ba)
new_merge_pairs0(:(vz118110, []), ba) → :(vz118110, [])
new_compare0(Neg(Zero), Neg(Zero)) → EQ
new_compare0(Neg(Succ(vz120000)), Pos(vz11900)) → LT
new_primCmpNat2(Zero, Zero) → EQ
new_merge1(vz117, :(vz11800, vz11801), :(vz118100, vz118101), ba) → new_merge2(vz117, new_merge00(vz118100, vz11800, vz11801, vz118101, new_compare14(vz11800, vz118100, ba), ba), ba)
new_compare(vz1170, vz11800, ty_Double) → new_compare9(vz1170, vz11800)
new_compare14(vz11800, vz118100, ty_Ordering) → new_compare10(vz11800, vz118100)
new_compare(vz1170, vz11800, app(app(ty_Either, bg), bh)) → new_compare6(vz1170, vz11800, bg, bh)
new_compare14(vz11800, vz118100, ty_Double) → new_compare9(vz11800, vz118100)
new_primCmpNat2(Zero, Succ(vz1190000)) → LT
new_compare14(vz11800, vz118100, app(ty_[], cc)) → new_compare8(vz11800, vz118100, cc)
new_merge00(vz127, vz128, vz129, vz130, GT, bf) → :(vz127, new_merge2(:(vz128, vz129), vz130, bf))
new_compare12(vz1170, vz11800, cd) → error([])
new_compare9(vz1170, vz11800) → error([])
new_primCmpNat1(Succ(vz119000), vz120000) → new_primCmpNat2(vz119000, vz120000)
new_compare14(vz11800, vz118100, ty_Integer) → new_compare13(vz11800, vz118100)
new_compare14(vz11800, vz118100, ty_Float) → new_compare4(vz11800, vz118100)
new_primCmpNat2(Succ(vz1200000), Zero) → GT
new_primCmpNat2(Succ(vz1200000), Succ(vz1190000)) → new_primCmpNat2(vz1200000, vz1190000)
new_compare0(Neg(Zero), Neg(Succ(vz119000))) → new_primCmpNat0(vz119000, Zero)
new_compare0(Pos(Succ(vz120000)), Neg(vz11900)) → GT
new_compare0(Neg(Succ(vz120000)), Neg(vz11900)) → new_primCmpNat1(vz11900, vz120000)
new_compare6(vz1170, vz11800, bg, bh) → error([])
new_primCmpNat0(vz120000, Zero) → GT
new_merge2([], :(vz11800, vz11801), ba) → :(vz11800, vz11801)
new_compare0(Pos(Zero), Neg(Succ(vz119000))) → GT
new_compare(vz1170, vz11800, ty_Int) → new_compare0(vz1170, vz11800)
new_merge_pairs0([], ba) → []
new_compare3(vz1170, vz11800, bc, bd, be) → error([])
new_compare4(vz1170, vz11800) → error([])
new_compare(vz1170, vz11800, app(ty_[], cc)) → new_compare8(vz1170, vz11800, cc)
new_compare0(Neg(Zero), Pos(Succ(vz119000))) → LT
new_compare(vz1170, vz11800, ty_Bool) → new_compare11(vz1170, vz11800)
new_merge1(vz117, vz1180, [], ba) → new_merge2(vz117, vz1180, ba)
new_merge2(:(vz1170, vz1171), :(vz11800, vz11801), ba) → new_merge00(vz11800, vz1170, vz1171, vz11801, new_compare(vz1170, vz11800, ba), ba)
new_compare(vz1170, vz11800, ty_@0) → new_compare5(vz1170, vz11800)
new_merge2(vz117, [], ba) → vz117
new_compare1(vz1170, vz11800) → error([])
new_compare0(Pos(Succ(vz120000)), Pos(vz11900)) → new_primCmpNat0(vz120000, vz11900)
new_compare8(vz1170, vz11800, cc) → error([])
new_compare14(vz11800, vz118100, app(app(ty_Either, bg), bh)) → new_compare6(vz11800, vz118100, bg, bh)
new_compare5(vz1170, vz11800) → error([])
new_compare11(vz1170, vz11800) → error([])
new_compare0(Pos(Zero), Pos(Succ(vz119000))) → new_primCmpNat1(Zero, vz119000)
new_compare(vz1170, vz11800, app(app(app(ty_@3, bc), bd), be)) → new_compare3(vz1170, vz11800, bc, bd, be)
new_compare(vz1170, vz11800, app(app(ty_@2, ca), cb)) → new_compare7(vz1170, vz11800, ca, cb)
new_compare(vz1170, vz11800, ty_Ordering) → new_compare10(vz1170, vz11800)
new_compare14(vz11800, vz118100, app(ty_Ratio, bb)) → new_compare2(vz11800, vz118100, bb)
new_compare0(Neg(Zero), Pos(Zero)) → EQ
new_compare0(Pos(Zero), Neg(Zero)) → EQ
new_merge00(vz127, vz128, vz129, vz130, EQ, bf) → :(vz128, new_merge2(vz129, :(vz127, vz130), bf))
new_primCmpNat1(Zero, vz120000) → LT
new_compare13(vz1170, vz11800) → error([])
new_compare0(Pos(Zero), Pos(Zero)) → EQ
new_compare14(vz11800, vz118100, ty_@0) → new_compare5(vz11800, vz118100)
new_compare14(vz11800, vz118100, app(app(app(ty_@3, bc), bd), be)) → new_compare3(vz11800, vz118100, bc, bd, be)

The set Q consists of the following terms:

new_compare8(x0, x1, x2)
new_compare0(Neg(Succ(x0)), Neg(x1))
new_merge1(x0, x1, [], x2)
new_compare0(Neg(Zero), Pos(Succ(x0)))
new_compare0(Pos(Zero), Neg(Succ(x0)))
new_primCmpNat0(x0, Succ(x1))
new_compare14(x0, x1, ty_Ordering)
new_compare0(Neg(Zero), Pos(Zero))
new_compare0(Pos(Zero), Neg(Zero))
new_primCmpNat0(x0, Zero)
new_compare(x0, x1, app(ty_Ratio, x2))
new_compare14(x0, x1, ty_Bool)
new_compare14(x0, x1, ty_Integer)
new_compare(x0, x1, ty_Int)
new_compare0(Pos(Succ(x0)), Pos(x1))
new_compare0(Neg(Zero), Neg(Zero))
new_merge_pairs0(:(x0, []), x1)
new_compare10(x0, x1)
new_compare12(x0, x1, x2)
new_compare0(Neg(Succ(x0)), Pos(x1))
new_compare0(Pos(Succ(x0)), Neg(x1))
new_compare11(x0, x1)
new_primCmpNat2(Succ(x0), Zero)
new_compare4(x0, x1)
new_compare14(x0, x1, app(ty_[], x2))
new_compare13(x0, x1)
new_compare14(x0, x1, app(ty_Maybe, x2))
new_primCmpNat2(Zero, Zero)
new_compare(x0, x1, ty_Integer)
new_primCmpNat2(Succ(x0), Succ(x1))
new_compare14(x0, x1, ty_@0)
new_compare(x0, x1, ty_Ordering)
new_compare(x0, x1, app(app(ty_@2, x2), x3))
new_compare2(x0, x1, x2)
new_merge00(x0, x1, x2, x3, EQ, x4)
new_compare(x0, x1, ty_Char)
new_compare5(x0, x1)
new_compare(x0, x1, ty_@0)
new_merge2(:(x0, x1), :(x2, x3), x4)
new_merge00(x0, x1, x2, x3, LT, x4)
new_compare14(x0, x1, ty_Int)
new_compare7(x0, x1, x2, x3)
new_merge1(x0, :(x1, x2), :(x3, x4), x5)
new_merge1(x0, [], :(x1, x2), x3)
new_merge_pairs0([], x0)
new_merge_pairs0(:(x0, :(x1, x2)), x3)
new_compare(x0, x1, app(ty_Maybe, x2))
new_compare14(x0, x1, ty_Char)
new_compare9(x0, x1)
new_compare1(x0, x1)
new_compare(x0, x1, app(app(ty_Either, x2), x3))
new_primCmpNat1(Succ(x0), x1)
new_compare14(x0, x1, app(app(ty_@2, x2), x3))
new_compare(x0, x1, ty_Double)
new_merge2(x0, [], x1)
new_compare14(x0, x1, app(app(ty_Either, x2), x3))
new_merge2([], :(x0, x1), x2)
new_compare14(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare(x0, x1, app(ty_[], x2))
new_compare(x0, x1, ty_Bool)
new_primCmpNat1(Zero, x0)
new_compare(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare3(x0, x1, x2, x3, x4)
new_compare14(x0, x1, ty_Double)
new_compare14(x0, x1, app(ty_Ratio, x2))
new_compare6(x0, x1, x2, x3)
new_compare(x0, x1, ty_Float)
new_merge00(x0, x1, x2, x3, GT, x4)
new_compare0(Pos(Zero), Pos(Succ(x0)))
new_compare0(Pos(Zero), Pos(Zero))
new_compare14(x0, x1, ty_Float)
new_compare0(Neg(Zero), Neg(Succ(x0)))
new_primCmpNat2(Zero, Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

case	cmp x y of
	GT	→ y : merge cmp (x : xs) ys
	_	→ x : merge cmp xs (y : ys)

merge0	y cmp x xs ys GT	= y : merge cmp (x : xs) ys
merge0	y cmp x xs ys _	= x : merge cmp xs (y : ys)